Back to University of Twente portal
| 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 |
Description
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.
References
- Timed Automata in UPPAAL (Digital version available here)