Group colloquium: Making a sanity checker for Uppaal

When: Feb. 14, 2019, 15:45-16:30

Where: Ravelijn 4237

Who: Ramon Onis

Uppaal is a prominent tool that can be used to model and verify timed systems.

However, where modern programming IDEs these days have advanced methods to detect human errors and bad practices, Uppaal lacks such functionality. This makes the modeling process in Uppaal error-prone. Mistakes may go undetected and can influence the behavior of the model, which might have serious consequences depending on the real-world system it represents.

To solve this problem, we introduce a sanity checker: a tool that automatically analyses the model for common made modeling errors, such as unreachable locations/edges, unwanted deadlocks and more.

We list the different types of errors for which we can develop sanity checks, look at the methods used to implement the sanity checks and finally look at the end result

	Home > News and Events > Events
<< EEMCS (EWI) Home News and Events » Group Colloquium » Events » In the Media People Research Education Vacancies Intranet Contact	Group colloquium: Making a sanity checker for Uppaal When: Feb. 14, 2019, 15:45-16:30 Where: Ravelijn 4237 Who: Ramon Onis Uppaal is a prominent tool that can be used to model and verify timed systems. However, where modern programming IDEs these days have advanced methods to detect human errors and bad practices, Uppaal lacks such functionality. This makes the modeling process in Uppaal error-prone. Mistakes may go undetected and can influence the behavior of the model, which might have serious consequences depending on the real-world system it represents. To solve this problem, we introduce a sanity checker: a tool that automatically analyses the model for common made modeling errors, such as unreachable locations/edges, unwanted deadlocks and more. We list the different types of errors for which we can develop sanity checks, look at the methods used to implement the sanity checks and finally look at the end result