Verification of clock synchronization algorithms: Experiments on a combination of deductive tools

Damián Barsotti; Leonor Prensa Nieto; Alwen Tiu

doi:10.1007/s00165-007-0027-6

Verification of clock synchronization algorithms: Experiments on a combination of deductive tools

Damián Barsotti, Leonor Prensa Nieto^*, Alwen Tiu

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

12 Citations (Scopus)

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.

Original language	English
Pages (from-to)	321-341
Number of pages	21
Journal	Formal Aspects of Computing
Volume	19
Issue number	3
DOIs	https://doi.org/10.1007/s00165-007-0027-6
Publication status	Published - Aug 2007

Access to Document

10.1007/s00165-007-0027-6

Cite this

@article{e135d9cccd0e4ba49931c639f3fb7bd2,

title = "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 [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.",

keywords = "Clock synchronization, Combination of deductive tools, Theorem proving, Verification",

author = "Dami{\'a}n Barsotti and Nieto, \{Leonor Prensa\} and Alwen Tiu",

year = "2007",

month = aug,

doi = "10.1007/s00165-007-0027-6",

language = "English",

volume = "19",

pages = "321--341",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery (ACM)",

number = "3",

}

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 - https://www.scopus.com/pages/publications/34547541212

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 -

Verification of clock synchronization algorithms: Experiments on a combination of deductive tools

Abstract

Access to Document

Other files and links

Fingerprint

Cite this