University of Twente Student Theses
Does your model make sense? : Automatic verification of timed systems
Onis, Ramon (2018) Does your model make sense? : Automatic verification of timed systems.
|
PDF
1MB |
| Abstract: | Timed automata are an important tool for modeling real-time systems. However, when timed systems become larger and more complex, modeling these systems becomes harder and error-prone. Making errors in such models and not detecting them might have serious consequences for the development of the system it resembles. Furthermore, the longer it takes to detect an error, the longer it takes to correct the error itself and reverse the consequences it might have caused. Therefore it is essential that the modeler is provided with ways to detect these mistakes in an easy way as early as possible. In this thesis, we present \textsc{UrPal} (\textit{`your pal'}), a tool that performs sanity checks for commonly made errors when developing timed automata in Uppaal. For these common errors, efficient methods to detect them and present results to the user in a helpful manner have been designed and implemented. Our solutions makes extensive use of model-driven engineering, in particular model transformations. We show that the designed implementations are sound and correct and evaluate the performance in order to choose the most efficient implementations. Furthermore, we apply the sanity checker to several (industrial) models to show the value of the sanity checker. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/77031 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page