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
Conference papers

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

Damian Barsotti 1 Leonor Prensa Nieto 1 Alwen Tiu 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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~\cite{lamport_cs} 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 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 first-order provers with support for arithmetic like ICS and CVC Lite.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000638
Contributor : Leonor Prensa Nieto Connect in order to contact the contributor
Submitted on : Thursday, November 10, 2005 - 2:01:26 PM
Last modification on : Friday, February 4, 2022 - 3:30:48 AM
Long-term archiving on: : Friday, April 2, 2010 - 6:56:19 PM

Identifiers

  • HAL Id : inria-00000638, version 1

Collections

Citation

Damian Barsotti, Leonor Prensa Nieto, Alwen Tiu. Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools. Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS '05, Ranko Lazic, Rajagopal Nagarajan, Nikolaos Papanikolaou, Sep 2005, Coventry/UK. ⟨inria-00000638⟩

Share

Metrics

Record views

101

Files downloads

185