Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive toolsReportar como inadecuado




Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 MOSEL - Proof-oriented development of computer-based systems INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

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 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~\cite{lamport cs} and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch, 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.

Keywords : Theorem proving verification clock synchronization





Autor: Damian Barsotti - Leonor Prensa Nieto - Alwen Tiu -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados