University of Twente Student Theses


Model validation for stochastic hybrid automata

Bakker, Michiel (2020) Model validation for stochastic hybrid automata.

[img] PDF
Abstract:A hybrid automaton is a mathematical formalism used to model systems with both discrete and continuous behaviour. The theory of hybrid automata has been applied in a wide spectrum of research areas, including systems biology, automotive and avionic control systems and other cyber-physical systems. One of the available tools to model hybrid automata is Uppaal SMC, which uses a simulation-based method named statistical model checking to verify properties of a model. As models grow larger and more complex, it becomes more likely for an error to be accidentally introduced to the system. The process of confirming that a model is free of errors is called model validation. However, little research has been done on model validation tools for hybrid automata. In this research, we examined several methods for model validation, and put them into practice in a tool for Uppaal SMC. The validation methods were examined using theoretical analysis and evaluated using case studies, which indicated that the tool provides an effective way of performing model validation.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:30 exact sciences in general, 54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page