Tempo: a model-checker for event-recording automata. We present a symbolic on-the-fly model checking algorithm for event-recording automata, a subclass of timed automata. This algorithm is based on a forward reachability analysis and uses a symbolic representation of clock constraints. It forms the core of the verification tool Tempo. We also develop a real-time logic for specifying properties of event-recording automata in a suitable way and demonstrate that the model checking problem for this logic is decidable.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Geeraerts, Gilles; Raskin, Jean-François; Sznajder, Nathalie: On regions and zones for event-clock automata (2014)
- Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
- Geeraerts, Gilles; Raskin, Jean-François; Sznajder, Nathalie: Event clock automata: From theory to practice (2011)
- Sorea, Maria: Bounded model checking for timed automata (2003)
- Møller, Jesper B.: DDDLIB: A library for solving quantified difference inequalities (2002)