A Zeno Run detection tool for UPPAAL

ZenoTool is a small, fast command-line tool that analyzes model specifications of timed automata systems created with UPPAAL for the occurrence of Zeno Runs.
Zeno Runs are paths in the timed transition system where infinite actions are executed in finite time. Since such behavior does not comply with real-world behavior, Zeno Runs often are unintentional. Moreover, timelocks, the counterpart to deadlocks in timed systems, may occur due to them.

ZenoTool was developed by Jonas Rinast during the work on his Diploma thesis, which is based on the strongly non-Zenoness property introduced by Tripakis [1], methods developed by Gómez and Bowman [2], and enhancements made in the thesis.

Find the original publication "Enhancing UPPAAL's Explanatory Power using Static Zeno Run Analysis" here.

In the thesis, 13 case study models were analyzed using ZenoTool. The models can be downloaded here. Copyrights belong to the original creators.

The regression test model used for validation is available here.

ZenoTool can be downloaded here (includes test model).

References:

[1] Stavros Tripakis. Verifying progress in timed systems. In ARTS'99, 5th International AMAST Workshop on Real-time and Probabilistic Systems, volume 1601 of Lecture Notes in Computer Science, pages 299-314. Springer-Verlag, May 1999.

[2] Rodolfo Gómez and Howard Bowman. Efficient Detection of Zeno Runs in Timed Automata. In J.-F. Raskin and P.S. Thiagarajan, editors, Proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2007), volume 4763 of LNCS, pages 195-210, Salzburg, Austria, October 2007. Springer.