author: Michiel Bakker
title: Model validation for Stochastic Timed Automata
keywords: Timed Automata, modelling, verification, model validation, stochastic model checking
topics: Other
committee: Rom Langerak
started: June 2019
end: August 2020


UPPAAL SMC is an extension to UPPAAL for modelling Networks of Stochastic Timed Automata (NSTA). It has been used in research areas such as systems biology, energy-centric systems, and recently, in modelling healthcare processes. However, as the models become larger and more complex, it becomes more likely for the modeller to make mistakes. It is therefore desirable to verify certain safety properties of the model, to make sure the model behaves as it should.

However, whereas verifying properties over (Networks of) Timed Automata is decidable, this is not the case for NSTAs. A solution to this is to reduce the NSTA to a pure UPPAAL NTA model, and use that model to verify safety properties. The limitation here is that NTAs are less expressive than NSTAs, which means that the reduced model can only be an approximation of the original model.

The objectives of this assignment is to develop a tool that converts UPPAAL SMC models to pure UPPAAL models, and reason about under which assumptions safety properties of the original model can be verified.