An Assertional Correctness Proof of a Self-Stabilizing l-Exclusion Algorithm
Venue
11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'06), IEEE CS (2006), pp. 199-208
Publication Year
2006
Authors
Milos Besta, Frank Stomp
BibTeX
Abstract
A formal correctness proof of a self-stabilizing l-exclusion algorithm (SLEX) is
described. The analyzed algorithm is an improvement of the SLEX due to Abraham,
Dolev, Herman, and Koll, since our version satisfies a stronger liveness property.
The proof is formulated in Linear-Time Temporal Logic and utilizes a history
variable to model access to regular registers. The proof consists of a safety part
and a liveness part. Our analysis provides some new insight in the correctness of
the algorithm: (1) Our proof is constructive. That is, we explicitly formulate
auxiliary quantities required to establish some of the properties. This contrasts
with the operational arguments of Abraham et al., where many quantities are not
explicitly formulated and the validity of the above mentioned properties is
established by disproving their non-existence. (2) We characterize processes (and
their minimum number) identified by some process as attempting to enter the
critical section. (3) A novel proof rule for reasoning about programs in the
presence of disabled processes is presented to structure the liveness proof.
