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 Mark 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 becompiled 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 shown that SpinJ is on average only 3.5 times slower than SPIN and it uses less memory in most of the cases.

Additional Resources

1. The paper