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

Formal Analysis for Dependability Properties:
the Time-Triggered Architecture Example

Holger Pfeifer and Friedrich W. von Henke

Presented at the
8th IEEE International Conference on
Emerging Technologies and Factory Automation (ETFA 2001)
Antibes Juan-les-Pins, France, October 15-18, 2001
© IEEE Computer Society


 Abstract

This paper describes the mechanized formal verification we have performed on some of the crucial algorithms used in the Time-Triggered Architecture (TTA) for safety-critical distributed control. We outline the approach taken to formally analyse the clock synchronization algorithm and the group membership service of TTA, summarize our experience and describe remaining challenges.

 Online Copy

  © 2001 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.
  Paper is available as Postscript (181 KB) or gzip'ed Postscript (67 KB)

 BibTeX Entry

 
@InProceedings{PvH01,
  author =    "Holger Pfeifer and Friedrich W. von Henke",
  title =     "{Formal Analysis for Dependability Properties: 
               the Time-Triggered Architecture Example}", 
  year =      2001,
  booktitle = "8th IEEE International Conference on 
               Emerging Technologies and Factory Automation (ETFA 2001)",
  editor =    "",
  pages =     "343--352",
  publisher = "IEEE",
  address =   "Antibes Juan-les-Pins",
  month =     "October"
}


Dept. of AI Homepage Research Help Mail to Webmaster H. Pfeifer - October 1, 2001