The two-step commitment protocol: Modeling, specification and proof methodology
J.-L. Baer, Georges Gardarin, Claude Girault, Gérard Roucairol · International Conference on Software Engineering · 1981
A two-step commitment algorithm which assures transaction update atomicity in a distributed data base is modelled using colored Petri Nets. The modeling helps in determining the numerous crash possibilities and in specifying recovery procedures and associated protocols. The use of unalterable logs is required and modelled accordingly. A methodology for proof correctness based on linear invariants is presented.