Incremental extension of the saturation algorithm-based bounded model checking of Petri nets

OData support
Vörös András
Department of Measurement and Information Systems

Nowadays, in safety critical and other applications the usage of formal methods, like model checking is more and more common in order to increase the quality.

However, the analysis of complex systems is a difficult task due to the existing resource limitations. This problem inspired many new model checking algorithms. One of them is the saturation-based algorithm which used to be efficient, especially for asynchronous systems, thanks to its compact data representation and special iteration strategy.

There exists a variant of the saturation-based algorithm that performs bounded state space exploration, which can be efficiently used to detect shallow problems. Nevertheless, the existing bounded model checker algorithm cannot run incrementally (therefore every iteration will be restarted completely).

In my thesis, I examine the theoretical background of Petri-net-based model checking and saturation-based algorithms: like model checking, Petri nets, decision diagrams and saturation-based algorithms.

I examine the previously published saturation-based bounded and unbounded state space exploration algorithms and model checking methods. I analyse the similarities and the challenges of the saturation-based algorithms. Moreover, I examine the new ideas of the algorithms and the properties that can be reused to be able to develop bounded incremental model checking algorithms.

In my work I designed two incremental model checking algorithms (the “continuing” and the “compacting” algorithms) which are two different ways to perform incremental model checking. I have also implemented these algorithms and compared their performance by measurements.


Please sign in to download the files of this thesis.