
Instances
of
Schneider's
generalized
protocol
of
clock
synchronization
Title: 
Instances of Schneider's generalized protocol of clock synchronization 
Author:

Damián Barsotti

Submission date: 
20060315 
Abstract: 
F. B. Schneider ("Understanding protocols for Byzantine clock synchronization") generalizes a number of protocols for Byzantine faulttolerant clock synchronization and presents a uniform proof for their correctness. In Schneider's schema, each processor maintains a local clock by periodically adjusting each value to one computed by a convergence function applied to the readings of all the clocks. Then, correctness of an algorithm, i.e. that the readings of two clocks at any time are within a fixed bound of each other, is based upon some conditions on the convergence function. To prove that a particular clock synchronization algorithm is correct it suffices to show that the convergence function used by the algorithm meets Schneider's conditions. Using the theorem prover Isabelle, we formalize the proofs that the convergence functions of two algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and MelliarSmith and the Faulttolerant Midpoint algorithm of LundeliusLynch, meet Schneider's conditions. Furthermore, we experiment on handling some parts of the proofs with fully automatic tools like ICS and CVClite. These theories are part of a joint work with Alwen Tiu and Leonor P. Nieto "Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools" in proceedings of AVOCS 2005. In this work the correctness of Schneider schema was also verified using Isabelle (entry GenClock in AFP). 
BibTeX: 
@article{ClockSynchInstAFP,
author = {Damián Barsotti},
title = {Instances of Schneider's generalized protocol of clock synchronization},
journal = {Archive of Formal Proofs},
month = mar,
year = 2006,
note = {\url{http://isaafp.org/entries/ClockSynchInst.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

