Verification of a Leader Election Algorithm in Timed Asynchronous Systems
The Timed Asynchronous System (TAS) model has less stringent assumptions than the synchronous model but is still strong enough to serve as a foundation for the construction of dependable applications. In this paper, we verify the correctness of some basic distributed services in TAS. First, TAS is modelled and then some important properties of two basic services, FADS (Fail Aware Datagram Service) and HALL (Highly Available Local Leader Election Service), are formally verified. The PVS theorem prover is used for modelling and verification of the algorithms.
During the process of verification, some of the assumptions in the model that were not explicitly noted in the literature came to light. In addition, due to the insight gained in the process of verification, the ability to extend the validity of some of the properties in the face of additional failures in the system became clear through appropriate modifications of these assumptions.
KeywordsTransmission Delay Local Leader Leader Election Partitionable System Clock Drift
Unable to display preview. Download preview PDF.
- 1.Christof Fetzer, “Fail Awareness in Timed Asynchronous Systems,” PhD thesis, CSE Dept, University of California, San Diego, 1997.Google Scholar
- 2.Nancy A. Lynch, “Distributed Algorithms,” Morgan Kaufmann,1996.Google Scholar
- 4.Flaviu Cristian, Christof Fetzer, “A Fail Aware Datagram Service,” 2 nd annual workshop on Parallel and Distributed Systems, April 5, 1997, Geneva, Switzerland.Google Scholar
- 5.John Rushby, “Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms,” IEEE Transactions on Software Engineering, vol. 25, no. 4, September 1999.Google Scholar
- 6.Natarajan Shankar, Sam Owre, John Rushby, D. W. J. Stringer Calvert, “PVS Prover Guide, Version 2.3,” September 1999.Google Scholar