Does your model make sense? Automated validation of timed automata

title:Does your model make sense? Automated validation of timed automata
keywords:timed automata, validation
topics:Dependability, security and performance
contact:E.J.J. Ruijters MSc & dr. M.I.A. Stoelinga


Timed Automata (TA) is a popular framework for modeling systems where time is important. Examples of such systems include network protocols, controllers for physical systems, and attack trees which describe possible ways a system could be compromised by a malicious attacker. TAs are very flexible and can be used for many different applications.

Unfortunately, this flexibility comes with a downside: There are many mistakes a modeler could make, and these mistakes are not always immediately obvious. Such mistakes include creating situations in which the system cannot do anything (deadlock), or constructing a model in which some important states can never be reached.

In this project you will develop a system for performing standard sanity checks on TAs, detecting many kinds of common mistakes and helping modelers avoid known pitfalls.


  1. Timed Automata in UPPAAL (Digital version available here)