A tool for the syntactic detection of Zeno-timelocks in timed automata. (English) Zbl 1272.68229

Bowman, Howard; Gomez, Rodolfo; Su, Li

Ulidowski, Irek (ed.), Proceedings of ARTS 2004, the 6th AMAST workshop on real-time systems (ARTS 2004), Stirling, UK, July 12, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 139, No. 1, 25-47 (2005).

Summary: Timed automata are a very successful notation for specifying and verifying real-time systems, but timelocks can freely arise. These are counter-intuitive situations in which a specifier’s description of a component automaton can inadvertently prevent time from passing beyond a certain point, possibly making the entire system stop. In particular, a Zeno-timelock represents a situation where infinite computation is performed in a finite period of time. Zeno-timelocks are very hard to detect for real-time model checkers, e.g., UPPAAL and Kronos. We have developed a tool which can take an UPPAAL model as input and return a number of loops which can potentially cause Zeno-timelocks. This tool implements an algorithm which refines a static verification approach introduced by Tripakis. We illustrate the use of this tool on a real-life case-study, the CSMA/CD protocol.
For the entire collection see [Zbl 1272.68037].

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q45	Formal languages and automata

Software:

Kronos; Uppaal; Uppaal2k