Property based model checking of structurally evolving Algebraic Petri nets

There are two important challenges in any system development life cycle, the first is to ensure the correctness of a model at the earliest stage possible and the second is to ensure its correctness once it evolves with respect to the emergence of new requirements, performance may need to be improve, business environment is changing. Usual verification techniques such as testing and simulation are used commonly for the verification of a model. The downsides of these techniques are that there is no guarantee of the absence of errors and they need to be repeated after every evolved version.
Model checking is an automatic technique for verifying finite state system models. Although, model checking is proved to be a useful technique, the typical drawback of model checking is its limits with respect to the state space explosion problem. As system gets reasonably complex, completely enumerating their states demands increasing amount of resources. Various techniques like symbolic model checking, on the fly model checking and compositional reasoning partially overcome this problem.
Petri net is a well-known low-level formalism for modeling and verifying concurrent and distributed systems. The modeling of systems by low-level Petri nets is tedious and therefore various advancements have been created to raise the level of abstraction of Petri nets. Among others, Algebraic Petri nets raise the level of abstraction of Petri nets by replacing black tokens with the elements of user defined data types i.e., algebraic abstract data types.
The first contribution of this thesis is to develop an approach to tackle the state space explosion problem for model checking of Algebraic Petri nets by re-using, adapting and refining state of the art techniques. The proposed approach is based on slicing and the central idea is to perform verification only on those parts that may affect the property the Algebraic Petri net model is analyzed for. We propose several slicing algorithms for Algebraic Petri nets and can be applied to Petri nets by slight modifications. The proposed slicing algorithms can alleviate the state space even for certain strongly connected nets and are proved not to increase the state space.
The second contribution is an approach to improving re-verification of structurally evolving Algebraic Petri nets. The idea is to classify evolutions and properties to identify which evolutions require re-verification. We argue that for the class of evolutions that require verification, instead of verifying the whole system, only a part that is concerned by the property can be sufficient.
The third contribution is the development of a stand-alone tool i.e., SLAPn. The objective of this tool is to implement proposed slicing algorithms and to show the practical usability of slicing technique. An interesting exploitation of SLAPn is that it can be added to any existing model checker as a pre-processing step.