| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [21 references]
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
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