author: Ramon Onis
title: Does your model make sense? Automated validation of timed automata
keywords: timed automata, validation
topics: Dependability, security and performance
committee: Arend Rensink ,
Mariëlle Stoelinga
started: February 2018
end: December 2018


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)

Additional Resources

  1. Thesis Ramon Onis