Abstract

In the field of formal verification we use model checkers to verify models of systems against a specification. Often these model checkers are specialised for a limited number of model specification languages, property specifications and verification algorithms. The purpose-built nature of these tools results in poor reusability, and in order to achieve optimisations the source code is generally not modular. As a result new tools are often developed from scratch and interoperability of tools is minimal.

This thesis presents a conceptual architecture for a framework to support these tools. This architecture is based on a layered design. A generic layer is to provide generic functionality for the simulation, testing and verification of models. An abstract layer provides a model implementation, such that it can use the functionality in the generic layer. Finally, a tool layer maps a particular model specification language to the abstract layer. The conceptual architecture has the objective to support reuse of code and to encourage a modular design in tools.

Besides the conceptual architecture, we also introduce a framework in the sense of a library. The design of this libary introduces an implementation of the conceptual architecture for explicit-state model checking. Firstly, a generic layer for explicit-state model checking with generic simulation and verification functionality is discussed. This generic layer uses type abstraction to abstract from the types of states, labels and transitions in the state spaces of the models.

Similarly, an abstract layer is introduced which uses a state representation based on graphs. We use the generic and abstract layer to model check PROM models. PROM is based on a minimalistic version of Promela, but adds the notion of shared pointer variables and dynamic object allocation.

Although the framework offers the flexibility and modularity for which is was made, the required verification time of the tool is significantly slower than SPIN. This can be ascribed to some design decisions that were made to make the framework more flexible. In particular this is the use of reference counting pointers and the design of the search module in the generic layer, and expensive operations in the abstract layer, such as linearisation and copying of the state graphs.

However, the statevector size achieved in our tool is generally smaller than those in SPIN using default settings and without any optimisations. This implies that potentially our tool is competitive with SPIN in terms of memory usage. Finally, the graph-based state representation enables the exploitation of symmetry reductions in the model. Thread-symmetry is exploited by means of a small change in the state linearisation procedure. This significantly reduces the number of visited states and only poses little overhead.

Additional Resources

1. The paper