The Time-Triggered Architecture is a distributed computer architecture for the implementation of highly dependable real-time systems specifically targeting embedded applications, such as digital control systems in the automotive and avionics domain. We have formally modelled and analysed various aspects of the underlying communication protocol TTP/C and its fault tolerance properties. This paper provides an overview of these analyses from a broader perspective and describes the relationships between the individual items. The algorithms implementing the basic protocol services of TTP/C are heavily intertwined and pose challenging problems for formal analysis. This is true not only with regard to the construction of formal proofs, but also for the development of the formal models themselves. We argue that an adequate structuring of the models and proofs along different levels of abstraction is necessary to enable the formal modelling of the central protocol algorithms, make their analysis feasible, and resolve the mutual dependencies among the services.

Online Copy

Available as Postscript (149 KB) or PDF (74 KB)

BibTeX Entry

@InProceedings{PvH04b, author = "Holger Pfeifer and Friedrich W. von Henke", title = "Formal Modelling and Analysis of Fault Tolerance Properties in the Time-Triggered Architecture", year = 2004, booktitle = "Proc. of the 5th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2004)", editor = "E. Schnieder and G. Tarnai", pages = "230-240", publisher = "Technical University of Braunschweig, Institute for Traffic Safety and Automation Engineering", month = "November" }