Verification of Clock Synchronization Algorithms: Experiments on a Combination of Deductive Tools

We report on an experiment in combining Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider's generalized clock synchronization protocol [13] in the theorem prover Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [9] and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch [10], satisfy Schneider's general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify the parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic tools like ICS and CVC-lite. Key words: Theorem proving, verification, clock synchroni...

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Damián Barsotti, Leonor Prensa Nieto, Alwen Fernanto Tiu
• Keywords: Algorithm, Clock Synchronization, Clock Synchronization Protocol, ENTCS 2006