Verification of clock synchronization algorithms: experiments on a combination of deductive tools |
| |
Authors: | Damián Barsotti Leonor Prensa Nieto Alwen Tiu |
| |
Affiliation: | (1) Universidad Nacional de Córdoba, Ciudad Universitaria, 5000 Córdoba, Argentina;(2) LORIA, 54506 Vandoeuvre-lès-Nancy, France;(3) Research School of Information Sciences and Engineering, Australian National University and National ICT Australia, Canberra, ACT, 0200, Australia |
| |
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: | Theorem proving Verification Clock synchronization Combination of deductive tools |
本文献已被 SpringerLink 等数据库收录! |
|