Sciweavers

FORMATS
2004
Springer

Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol Using Calendar Automata

14 years 2 months ago
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.
Bruno Dutertre, Maria Sorea
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where FORMATS
Authors Bruno Dutertre, Maria Sorea
Comments (0)