Society. Formal Verification for Time-Triggered Clock Synchronization

Distributed dependable real-time systems crucially depend on fault-tolerant clock synchronization. This paper reports on the formal anal-ysis of the clock synchronization service provided as an integral feature by the Time-Triggered Protocol (TTP), a communication protocol par-ticularly suitable for safety-critical control applications, such as in au-tomotive “by-wire ” systems. We describe the formal model extracted from the TTP specification and its formal verification, using the PVS system. Verification of the central clock synchronization properties is achieved by linking the TTP model of the synchronization algorithm to a generic derivation of the properties from abstract assumptions, es-sentially establishing the TTP algorithm as a concrete instance of the generic one by verifying that it satisfies the abstract assumptions. We also show how the TTP algorithm provides the clock synchronization that is required by a previously proposed general framework for verify-ing time-triggered algorithms.