Modeling and Verification of a Fault-Tolerant Real-time Startup
Protocol using Calendar Automata
Bruno Dutertre and Maria Sorea
Presented at FTRTFT '04,
Grenoble, France, September 2004. Appears in Springer Verlag LNCS 3253, pp. 199-214.
Abstract
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.
plain postscript,
or
PDF
SAL Files
Here
BibTeX Entry
@inproceedings{Dutertre&Sorea04,
AUTHOR = {Bruno Dutertre and Maria Sorea},
TITLE = {Modeling and Verification of a Fault-Tolerant
Real-time Startup Protocol using Calendar Automata},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
TITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ADDRESS = {Grenoble, France},
VOLUME = 3253,
YEAR = 2004,
MONTH = sep
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page