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

Springer LNCS 1486, Sept. 1998

© Springer-Verlag

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

Online Copy |

PVS FTRTFT 98 paper: ftrtft98.ps.gz

PVS specification files: clock.dmp

BibTeX Entry |

@InProceedings{ftrtft98,

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 |