Skip to main content
SpringerLink
Log in

Mechanical verification of clock synchronization algorithms

  • Selected Presentations
  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1486))

Abstract

Clock synchronization algorithms play a crucial role in a variety of fault-tolerant distributed architectures. Although those algorithms are similar in their basic structure, the particular designs differ considerably, for instance in the way clock adjustments are computed. This paper develops a formal generic theory of clock synchronization algorithms which extracts the commonalities of specific algorithms and their correctness arguments; this generalizes previous work by Shankar and Miner by covering non-averaging adjustment functions, in addition to averaging algorithms. The generic theory is presented as a set of parameterized PVS theories, stating the general assumptions on parameters and demonstrating the verification of generic clock synchronization. The generic theory is then specialized to the class of algorithms using averaging functions, yielding a theory that corresponds to those of Shankar and Miner. As examples of the verification of concrete, published algorithms, the formal verification of an instance of an averaging algorithms (by Welch and Lynch [3]) and of a non-averaging algorithm (by Srikanth and Toueg [14]) is discussed.

This work has been supported in part by ESPRIT LTR Project 20072 “Design for Validation (DeVa)” and ESPRIT Project 20716 “GUARDS’.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Kopetz and G. Gruensteidl. Ttp — a time triggered protocol for fault-tolerant real-time systems. IEEE Computer, 27(1):14–23, January 1994.

    Google Scholar 

  2. Hermann Kopetz. The time-triggered approach to real-time system design. In B. Randell, J.-C. Laprie, H. Kopetz, and B. Littlewood, editors, Predictably Dependable Computing Systems. Springer, 1995.

    Google Scholar 

  3. J. Lundelius Welch and N. Lynch. A new fault-tolerant algorithm for clock synchronization. Inf. and Comp., 77(1):1–36, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  4. P. S. Miner. Verification of fault-tolerant clock synchronization systems. NASA Technical Paper 3349, NASA Langley Research Center, Nov. 1993.

    Google Scholar 

  5. S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Computer-Aided Verification, CAV ’96, volume 1102 of Lecture Notes in Computer Science, pages 411–414, New Brunswick, NJ, July/August 1996. Springer-Verlag.

    Google Scholar 

  6. S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Trans. on Software Engineering, 21(2):107–125, February 1995.

    Article  Google Scholar 

  7. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer-Verlag.

    Google Scholar 

  8. D. Powell. A Generic Upgradable Architecture for Real-Time Dependable Systems. In IEEE Intern. Workshop on Embedded Fault-Tolerant Systems, Boston. May 1998.

    Google Scholar 

  9. J. Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. In M. Dal Cin, C. Meadows, and W. H. Sanders, editors, Dependable Computing for Critical Applications—6, pages 203–222. IEEE Computer Society, March 1997.

    Google Scholar 

  10. J. M. Rushby and F. von Henke. Formal verification of algorithms for critical systems. IEEE Trans. on Software Engineering, 19(1):13–23, Jan. 1993.

    Article  Google Scholar 

  11. F. B. Schneider. Understanding protocols for byzantine clock synchronization. Technical Report 87-859, Cornell University, Aug. 1987.

    Google Scholar 

  12. D. Schwier and F. von Henke. Mechanical verification of clock synchronization algorithms. Ulmer Informatik Berichte, UniversitÄt Ulm, 1998 (forthcoming).

    Google Scholar 

  13. N. Shankar. Mechanical verification of a schematic byzantine clock synchronization algorithm. Technical Report CR-4386, NASA, 1991.

    Google Scholar 

  14. T. K. Srikanth and S. Toueg. Optimal clock synchronization. Journ. of the ACM, 34(3):626–645, July 1987.

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FakultÄt für Informatik, UniversitÄt Ulm, D-89069, Ulm, Germany

    D. Schwier & F. von Henke

Authors
  1. D. Schwier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. F. von Henke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Anders P. Ravn Hans Rischel

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schwier, D., von Henke, F. (1998). Mechanical verification of clock synchronization algorithms. In: Ravn, A.P., Rischel, H. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1998. Lecture Notes in Computer Science, vol 1486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055353

Download citation

  • DOI: https://doi.org/10.1007/BFb0055353

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65003-4

  • Online ISBN: 978-3-540-49792-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation