Verification of clock synchronization algorithms: Experiments on a combination of deductive tools
Date
2007
Authors
Barsotti, Damian
Prensa-Nieto, Leonor
Tiu, Alwen
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
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 [Sch87] 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 [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch [LL84], 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.
Description
Keywords
Keywords: Automation; Computer aided software engineering; Synchronization; Theorem proving; Clock synchronization; Deductive tools; Schneider's generalized clock synchronization protocols; Algorithms Clock synchronization; Combination of deductive tools; Theorem proving; Verification
Citation
Collections
Source
Formal Aspects of Computing
Type
Journal article
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31
Downloads
File
Description