Description

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.