University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Our PVS papers

Modular Formal Analysis of the
Central Guardian in the Time-Triggered Architecture

Holger Pfeifer, Friedrich W. von Henke

Proc. of the
23rd International Conference on
Computer Safety, Reliability and Security (SAFECOMP)
Potsdam, Germany, September 21-24, 2004
© Springer-Verlag


 Abstract

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"
}


Dept. of AI Homepage Research Help Mail to Webmaster H. Pfeifer - September 27, 2004