HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools

Abstract : We report on an experiment in combining the theorem prover 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 in 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 and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch, satisfy Schneider's general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify 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 first-order provers with support for arithmetics.
Document type :
Journal articles
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/inria-00097383
Contributor : Leonor Prensa Nieto Connect in order to contact the contributor
Submitted on : Thursday, September 21, 2006 - 2:53:26 PM
Last modification on : Friday, February 4, 2022 - 3:30:17 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 1:06:29 AM

Identifiers

Collections

Citation

Damian Barsotti, Leonor Prensa Nieto, Alwen Tiu. Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools. Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.321-341. ⟨10.1007/s00165-007-0027-6⟩. ⟨inria-00097383⟩

Share

Metrics

Record views

51

Files downloads

276