High-level Petri net model checking : the symbolic way

Although model checking is heavily used in the hardware domain, its use is not mainstream in software engineering yet. Modeling of software system is tedious using low-level formalisms such as Place/Transition Petri Nets. Moreover, usual verification techniques (e.g., state space analysis) are often intractable because of the infamous State Space Explosion. While modeling can be eased by using high-level formalisms such as High- level Petri Nets that make models more concise and more readable, State Space Explosion is still an important challenge. Many authors have tackled this issue on High-level Petri Nets, mostly by either modularizing the system or by reducing the states to consider (e.g., partial orders, symmetries). Most of those approaches encode the state space explicitly, i.e., the required amount of memory is linear to the number of states, which is rapidly intractable due to State Space Explosion. Symbolic Model Checking partially overcomes this problem by encoding the state space in a condensed way using Decision Diagrams and has been success- fully applied to Place/Transition Petri Nets. Albeit very effective, to be applied to High-level Petri Nets, these techniques require to “unfold” the High-level Petri Nets to an equivalent Petri nets. This is sometimes impractical because it might be difficult, if not infeasible, to figure out the data types boundaries. To partially overcome these problems, we propose to apply Symbolic Model Checking at the High-level Petri Net level directly. To that end, we propose the S Decision Diagrams a kind of Decision Diagrams especially created to han- dle large sets of terms representing the instances of the data types. Besides, we introduce the notion of Partial Net Unfolding that avoids having to unfold all data types prior model checking. Moreover, we describe Algebraic Clustering that adapts the concept of clustering to High-level Petri Nets and therefore that allows to apply advanced techniques such as saturation. These contributions pave the way to the application of Symbolic Model Checking to modular extensions of the High-level Petri Net. Finally, as a proof of concept, we implemented all the proposed techniques in a model checker called the Algebraic Petri Nets Analyzer