University of Twente Student Theses
Bit-packing and Hashing Evaluation in Explicit-state Model Checking
Hol, Valentijn (2022) Bit-packing and Hashing Evaluation in Explicit-state Model Checking.
|
PDF
1MB |
| Abstract: | MCSTA is a model checking tool for models written in the Modest language. It can be used to formally verify certain properties of a model. During model checking a model’s state space needs to be (exhaustively) explored which takes a significant amount of time and memory – depending on model complexity. This research evaluates the impact of bit-packing state member variables by examining the execution time and memory consumption. We find that in all cases there is a decrease in memory usage, and in most cases a minor decrease in execution time. Furthermore, we propose an algorithm for selective field unpacking, to improve the performance of bit-packing, whilst maintaining near-optimal state sizes. Lastly, we evaluate the current hash function used in state space exploration based on hash-table bucket lengths, and find it to be performing adequately with little room for improvement. |
| 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: | https://purl.utwente.nl/essays/91885 |
| 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