Abstract

State space generation or reachability analysis plays an important role in model checking, but a disadvantage of current techniques lies in the fact that they require quite a lot of time and memory to come up with a result when using real-life system models. Symbolic state space generation using known traversal techniques as breadth-first search and chaining are quite common practice, but their performance on real-life system models with a large transition relation remains an issue to be tackled. In the past decade a relatively new traversal technique has emerged, named Saturation. This traversal technique has proven itself to be a good competitor to traditional symbolic state space generation techniques for handling models with extremely large state spaces. It originates from the research group of professor Gianfranco Ciardo (University of California at Riverside, USA).

The main goal of this Master project is to design and implement the aforementioned Saturation-based approach in the LTSmin toolset, which is a set of verification tools developed by the Formal Methods and Tools group (FMT) at the University of Twente. The main features of this toolset is its setup in architectural layers to separate language-specific details from verification algorithms and the use of an interface for presenting the (partitioned) transition relation of the model, called PINS.

The goal includes making adjustments to the LTSmin architecture for Saturation to work properly and comparing the implemented Saturation algorithm with other available symbolic reachability techniques in the LTSmin toolset.

An analysis of the Saturation-based approaches by G. Ciardo and the architecture of the LTSmin toolset is performed to choose the Saturation approach which fits best into the LTSmin toolset. The chosen (stand-alone) Saturation algorithm is then adjusted for implementation. The first version of this adjusted algorithm takes a different approach when updating the partitioned transition relation of the model compared to the algorithm proposed by G. Ciardo and reuses available functionality from the LTSmin toolset. An evaluation of this first version of the Saturation algorithm is performed comparing it to the other available reachability methods breadth-first search, chaining and an LTSmin version of a Saturation- like approach.

The evaluation reveals that the update process of the partitioned transition relation does not perform well for complex models resulting in bad time performance. Therefore the update process of the partitioned transition relation is revised. Hereby inspiration is taken from the update process used by G. Ciardo. This has resulted in a Saturation algorithm that outperforms the previous version of this Saturation algorithm and comes out on top of the traditional traversal techniques breadth-first search and chaining with regard to time performance. Compared to the LTSmin version of a Saturation-like algorithm it performs competitively well too.

Furthermore an existing reachability option of the LTSmin toolset which basically computes fix-points has been readjusted to make use of Saturation, where updates to the partitioned transition relation is done outside Saturation. This algorithm turns out to perform as good as well compared to breadth-first search and chaining, but not as great as the revised version of the stand-alone Saturation algorithm. A similar result is obtained as with the stand-alone Saturation algorithm when compared to the LTSmin version of a Saturation-like algorithm.

Additional Resources

1. The paper