zbMATH — the first resource for mathematics

Static detection of Zeno runs in UPPAAL networks based on synchronization matrices and two data-variable heuristics. (English) Zbl 1374.68298
Jurdziński, Marcin (ed.) et al., Formal modeling and analysis of timed systems. 10th international conference, FORMATS 2012, London, UK, September 18-20, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33364-4/pbk). Lecture Notes in Computer Science 7595, 220-235 (2012).
Summary: This paper addresses Zeno runs, i.e., transition sequences that can execute arbitrarily fast, in the context of model checking with the UPPAAL tool. Zeno runs conflict with real-world experience where execution always takes time and they may introduce timelocks into the models. We enhance previous work on static detection of Zeno runs by extending synchronization exploitation using a synchronization matrix that not only ensures valid synchronization partners exist but also that their number is correct. Additionally, we introduce two data-variable heuristics into the analysis as in most models data-variable constraints prevent certain Zeno runs. The analysis is implemented in a tool called ZenoTool and empirically evaluated using 13 benchmarks. The evaluation shows that our analysis is more accurate in 3 cases and never less accurate than the analysis results of previous work and that performance and memory overhead are at the same time very low.
For the entire collection see [Zbl 1251.68022].

68Q60 Specification and verification (program logics, model checking, etc.)
68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
68Q45 Formal languages and automata
ZenoTool; Uppaal; Kronos
Full Text: DOI