Distributed dependable real-time systems crucially depend on fault-tolerant clock synchronization. This paper reports on the formal analysis of the clock synchronization service provided as an integral feature by the Time-Triggered Protocol (TTP), a communication protocol particularly suitable for safety-critical control applications, such as in automotive "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, essentially 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 verifying time-triggered algorithms.

Online Copy

© 1999 IEEE. This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Available as Postscript (133 KB) or gzip'ed Postscript (48 KB).

BibTeX Entry

@InProceedings{PSvH:99:DCCA7, author = "Holger Pfeifer and Detlef Schwier and Friedrich W.~von Henke", title = "{Formal Verification for Time-Triggered Clock Synchronization}", editor = "Charles B. Weinstock and John Rushby (eds.)", series = "Dependable Computing and Fault-Tolerant Systems", volume = "12", pages = "207--226", booktitle = "Dependable Computing for Critical Applications 7", year = 1999, publisher = "IEEE Computer Society", month = jan }