We present a modular formal analysis of the communication properties of the Time-Triggered Protocol TTP/C based on the guardian approach. The guardian is an independent component that employs static knowledge about the system to transform arbitrary node failures into failure modes that are covered by the rather optimistic fault hypothesis of TTP/C. Through a hierarchy of formal models, we give a precise description of the arguments that support the desired correctness properties of TTP/C. First, requirements for correct communication are expressed on an abstract level. By stepwise refinement we show that the abstract requirements are met under the optimistic fault hypothesis, and how the guardian model allows a broader class of failures be tolerated.

Online Copy

Paper: Available as Postscript (318 KB) or PDF (129 KB) PVS specification and proof files (for PVS Version 3.1): Save the dump file safecomp2004.dump (149 KB) in a new directory. Unpack the theories with M-x undump-pvs-files within PVS. The top-level theory is top.pvs.

BibTeX Entry

@InProceedings{PvH04, author = "Holger Pfeifer and Friedrich W. von Henke", title = "Modular Formal Analysis of the Central Guardian in the Time-Triggered Architecture", year = 2004, booktitle = "Proc. of the 23rd International Conference on Computer Safety, Reliability, and Security (SAFECOMP)", editor = "Maritta Heisel and Peter Liggesmeyer and Stefan Wittmann", pages = "240--253", series = "Lecture Notes in Computer Science", volume = 3219, publisher = "Springer-Verlag", address = "Potsdam, Germany", month = "September" }