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

Damian Barsotti 1 Leonor Prensa Nieto 2 Alwen Tiu 3
1 FaMAF - Facultad de Matemática, Astronomía y Física [Cordoba]
2 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 Research School of Information Sciences and Engineering
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.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.321-341. 〈10.1007/s00165-007-0027-6〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00097383
Contributeur : Leonor Prensa Nieto <>
Soumis le : jeudi 21 septembre 2006 - 14:53:26
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : mardi 6 avril 2010 - 01:06:29

Fichier

fac07.pdf

Identifiants

Collections

INRIA | LORIA | UNIV-LORRAINE

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

159

Téléchargements de fichiers

276

Contact


archive-ouverte@inria.fr