title: Does your model make sense? Automated validation of timed automata
keywords: timed automata, validation
topics: Dependability, security and performance
committee: Enno Ruijters ,
Mariƫlle 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)