Property based model checking of structurally evolving Algebraic Petri nets

Doctoral thesis (2015)

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 ... [more ▼]

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. [less ▲]

Slicing High-level Petri nets

Report (2014)

Optimizing verification of structurally evolving algebraic petri nets

in Lecture Notes in Computer Science (2013, September 08), 8166

System models are subject to evolve during the development life cycle, along which an initial version goes through a series of evolutions, generally aimed at progressively reaching all the requested ... [more ▼]

System models are subject to evolve during the development life cycle, along which an initial version goes through a series of evolutions, generally aimed at progressively reaching all the requested qualities (completeness, correctness etc.). Among the existing development methodologies the iterative and incremental one has been proved to be efficient for system development but lacks of support for an adequate verification process. When considering Algebraic Petri nets (APNs) for modeling and model checking for verification, all the proofs must be redone after each iteration which is impractical both in terms of time and space. In this work, we introduce an Algebraic Petri net slicing technique that optimizes the model checking of static or structurally evolving APN models. Furthermore, our approach is proposing a classification of evolutions dedicated to the improvement of model checking. [less ▲]

Optimizing algebraic petri net model checking by slicing

in International Workshop on Modeling and Business Environments (ModBE’13) in Milano, Italy, June 24, 2013. (2013)

High-level Petri nets make models more concise and read- able as compared to low-level Petri nets. However, usual verification techniques such as state space analysis remain an open challenge for both ... [more ▼]

High-level Petri nets make models more concise and read- able as compared to low-level Petri nets. However, usual verification techniques such as state space analysis remain an open challenge for both because of state space explosion. The contribution of this paper is to propose an approach for property based reduction of the state space of Algebraic Petri nets (a variant of high-level Petri nets). To achieve the objective, we propose a slicing algorithm for Algebraic Petri nets (APNSlicing). The proposed algorithm can alleviate state space even for certain strongly connected nets. By construction, it is guaranteed that the state space of sliced net is at most as big as the original net. We exemplify our technique through the running case study of car crash management system. [less ▲]

Optimizing algebraic petri net model checking by slicing

Report (2013)

A formal approach for engineering resilient car crash management system

Report (2012)