TY - JOUR
T1 - Verification of clock synchronization algorithms
T2 - Experiments on a combination of deductive tools
AU - Barsotti, Damián
AU - Nieto, Leonor Prensa
AU - Tiu, Alwen
PY - 2007/8
Y1 - 2007/8
N2 - 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.
AB - 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.
KW - Clock synchronization
KW - Combination of deductive tools
KW - Theorem proving
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=34547541212&partnerID=8YFLogxK
U2 - 10.1007/s00165-007-0027-6
DO - 10.1007/s00165-007-0027-6
M3 - Article
SN - 0934-5043
VL - 19
SP - 321
EP - 341
JO - Formal Aspects of Computing
JF - Formal Aspects of Computing
IS - 3
ER -