Model-Checking Fault-Tolerant Clock Synchronization Protocols

VCLA will be hosting a RiSE seminar talk by Wilfried Steiner on April 11th, 2013.

ABSTRACT

Clock synchronization is the foundation of distributed real-time architectures such as the Timed-Triggered Architecture. Maintaining the local clocks synchronized is particularly important for fault tolerance, as it allows one to use simple and effective fault-tolerance algorithms that have been developed in the synchronous system model.

Clock synchronization algorithms have been extensively studied since the 1980s, and many fundamental results have been established. Traditionally, the correctness of a new clock synchronization algorithm is shown by reduction to these results. Until now, formal proofs of correctness all relied on interactive theorem provers such as PVS or Isabelle/HOL. In this talk, we discuss an automated proof of the TTEthernet clock-synchronization algorithm that is based on the SAL model checker. Furthermore, we present how the formal models and proofs can be reused in the verification of more advanced algorithms.