University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Our Papers

Mechanical Verification of Clock Synchronization Algorithms

D. Schwier, F.W. von Henke

Appeared in: Proc. FTRTFT'98, 5th Intl. Symp. Formal Techniques in Real-Time Fault-Tolerant Systems
Springer LNCS 1486, Sept. 1998
© Springer-Verlag


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) and of a non-averaging algorithm (by Srikanth and Toueg) is discussed.

 Online Copy

PVS FTRTFT 98 paper:

PVS specification files:  clock.dmp

 BibTeX Entry

  author = {Detlef Schwier and Friedrich von Henke},
  title = {Mechanical Verification of Clock Synchronization Algorithms},
  booktitle = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
  pages = {262--271},
  year = 1998,
  editor = {Anders P. Ravn and Hans Rischel},
  number = 1486,
  series = {LNCS},
  month = {September},
  publisher = {Springer} }

Dept. of AI Homepage Research Help Mail to Webmaster - Sep. 11, 1998