Verification of Clock Synchronization Algorithms: Experiments on a Combination of Deductive Tools

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 [Schneider, F. B., Understanding protocols for Byzantine clock synchronization, Technical Report TR 87–859, Cornell University (1987). URL citeseer.ist.psu.edu/schneider87understanding.html] 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 [Lamport, L. and P. M. Melliar-Smith, Synchronizing clocks in the presence of faults, J. ACM 32 (1985), pp. 52–78] and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch [Lundelius, J. and N. Lynch, A new fault-tolerant algorithm for clock synchronization, in: Proceedings of PODC '84 (1984), pp. 75–88], satisfy Schneider's general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify the 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 arithmetic like ICS and CVC Lite