University of Twente Student Theses


Converting Modest Models to Efficient Code

Heyns, L. (2020) Converting Modest Models to Efficient Code.

[img] PDF
Abstract:Model checking is an automated technique that, given a finite-state model of a system and a formal property, systematically checks whether this property holds for (a given state in) that model. The Modest Toolset can be used to study the reliability and performance of systems through model checking. One of the features in the Modest Toolset is converting the models to a code representation, which allows easier writing of algorithms using those models. This feature is currently used in a teaching setting, the generated code facilitates interacting with models such that the students can write their own model checking algorithms. The current implementation generates slow code and is limited to only generating Python. This paper shows methods to make the code generated by the Modest Toolset faster, which allows more complex models to be checked, and to allow it to generate models in more programming languages, which makes creating model checking algorithms accessible to a wider public; it will then compare the performance of model checking in these different programming languages.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page