|title:||Does your model make sense? Automated validation of timed automata|
|keywords:||timed automata, validation|
|topics:||Dependability, security and performance|
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.
- Timed Automata in UPPAAL (Digital version available here)