Modeling and Verification of a Fault-Tolerant Real-time Startup Protocol using Calendar Automata

We discuss the modeling and verification of real-time systems using the SAL model checker. A new modeling framework based on event calendars enables dense timed systems to be described without relying on continuously varying clocks. We present verification techniques that rely on induction and abstraction, and show how these techniques are efficiently supported by the SAL symbolic model-checking tools. The modeling and verification method is applied to the fault-tolerant real-time startup protocol used in the Timed Triggered Architecture.

Online Copy

	© 2004 Springer-Verlag.
	Paper is available as Postscript (179 KB) or gzip'ed Postscript (69 KB)

BibTeX Entry

@InProceedings{DS:FTRTFT04, author = "Bruno Dutertre and Maria Sorea", title = "{Modeling and Verification of a Fault-Tolerant Real-time Startup Protocol using Calendar Automata}", year = 2004, booktitle = "Proc. of the Joint Conference Formal Modelling and Analysis of Timed Systems (FORMATS), Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT)", editor = "", pages = "", series = "Lecture Notes in Computer Science", volume = "", publisher = "Springer-Verlag", month = sep }