Formal Verification of the Ricart-Agrawala Algorithm

Ekaterina Sedletsky Amir Pnueli Mordechai Ben-Ari

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


This paper presents the formal verification of the Ricart-Agrawala algorithm for distributed mutual exclusion of an arbitrary number of nodes. It uses the Temporal Deductive 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 eficient notation is introduced to facilitate the presentation of liveness proofs by verification diagrams. The proofs were carried out using the Stanford Temporal Prover (STeP) [BBC95], a software package that supports formal verification of temporal specifications of concurrent and reactive systems.

Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Start Conference Manager
Conference Systems