Sciweavers

Share
FSTTCS
2000
Springer

Formal Verification of the Ricart-Agrawala Algorithm

9 years 7 months ago
Formal Verification of the Ricart-Agrawala Algorithm
Abstract. This paper presents the first formal verification of the RicartAgrawala algorithm [RA81] for distributed mutual exclusion of an arbitrary number of nodes. It uses the Temporal Methodology of [MP95a]. We establish both the safety property of mutual exclusion and the liveness property of accessibility. To establish these properties for an arbitrary number of nodes, parameterized proof rules are used as presented in [MP95a] (for safety) and [MP94] (for liveness). A new and efficient notation is introduced to facilitate the presentation of liveness proofs by verification diagrams. The proofs were carried out using the Stanford Temporal Prover (STeP) [BBC+ 95], a software package that supports formal verification of temporal specifications of concurrent and reactive systems.
Ekaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ar
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where FSTTCS
Authors Ekaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ari
Comments (0)
books