University of Twente Student Theses
The SpinJ model checker : a fast, extensible, object-oriented model checker
Jonge, Marc de (2008) The SpinJ model checker : a fast, extensible, object-oriented model checker.
![[img]](http://essay.utwente.nl/style/images/fileicons/application_pdf.png) |
PDF
769kB |
| Abstract: | Model checking has grown to be a practical addition to the field of formal verification. One model checker that has proven itself very useful in practice is Spin, which is built to validate models that are written in promela. It can be used to search for deadlocks, assertions, liveness properties and even LTL properties. This thesis describes the design and implementation of SpinJ, a reimplementation of Spin in Java. SpinJ is designed to be behave similarly to Spin, but to be more extendible and reusable. To achieve this the conceptual framework of Kattenbelt is used as the basis for the design of the SpinJ library, using the three layers that he describes. Firstly, the generic layer is the lowest layer which uses a basic model with states and transitions. On this layer all storage methods, search algorithms and simulation techniques are implemented. The abstract layer describes a concurrent model with processes that is an extension of the model in the generic layer. This knowledge of processes within the model makes it possible to implement partial order reduction here. Finally the tool layer is implemented for the promela language support. SpinJ also contains a promela compiler that generates Java code to represent the given promela model. This Java code can be compiled and then verified using the SpinJ library. Since this library contains all the actual algorithms, the generated code can be relatively small, only describing the model itself. Also all algorithms that are available can be used with any model and can be selected at runtime. Despite the fact that SpinJ is designed to be extendible and reusable, it is not slow; using the BEEM benchmark, this thesis has shows that SpinJ is on average only 3.5 times slower than Spin and it uses less memory in most of the cases. |
| Item Type: | Essay (Master) |
| Clients: | TNO |
| 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/58409 |
| 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