Advertisement

Verification of a Leader Election Algorithm in Timed Asynchronous Systems

  • Neeraj Jaggi
  • K. Gopinath
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2245)

Abstract

The Timed Asynchronous System (TAS) model[3] 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.

Keywords

Transmission Delay Local Leader Leader Election Partitionable System Clock Drift 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Christof Fetzer, “Fail Awareness in Timed Asynchronous Systems,” PhD thesis, CSE Dept, University of California, San Diego, 1997.Google Scholar
  2. 2.
    Nancy A. Lynch, “Distributed Algorithms,” Morgan Kaufmann,1996.Google Scholar
  3. 3.
    Flaviu Cristian, Christof Fetzer, “The Timed Asynchronous Distributed System Model,” IEEE Transaction on Parallel and Distributed Systems, vol. 10, no. 6, pp. 642–657, June 1999.CrossRefGoogle Scholar
  4. 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. 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. 6.
    Natarajan Shankar, Sam Owre, John Rushby, D. W. J. Stringer Calvert, “PVS Prover Guide, Version 2.3,” September 1999.Google Scholar
  7. 7.
    Flaviu Cristian, Christof Fetzer, “A Highly Available Local Leader Election Service,” IEEE Transactions on Software Engineering, vol. 25, no. 5, pp. 603–618, September/October 1999.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Neeraj Jaggi
    • 1
  • K. Gopinath
    • 1
  1. 1.Indian Institute of ScienceIndia

Personalised recommendations