Sciweavers

ENTCS
2006

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

13 years 11 months ago
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...
Damián Barsotti, Leonor Prensa Nieto, Alwen
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Damián Barsotti, Leonor Prensa Nieto, Alwen Fernanto Tiu
Comments (0)