StrataGEM: A Generic Petri Net Verification Framework

TitleStrataGEM: A Generic Petri Net Verification Framework
Publication TypeConference Paper
Year of Publication2014
AuthorsBóbeda, Edmundo López, Colange Maximilien, and Buchs Didier
EditorCiardo, Gianfranco, and Kindler Ekkart
Conference NameProceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency
Date Published06/2014
Conference LocationTunis, Tunisia

In this paper we present the Strategy Generic Extensible Modelchecker (StrataGEM), a tool aimed at the analysis of Petri nets and other models of concurrency by means of symbolic model-checking techniques. StrataGEM marries the well know concepts of Term Rewrit- ing (TR) to the efficiency of Decision Diagrams (DDs). TR systems are a great way to describe the semantics of a system, being readable and com- pact, but their direct implementation tends to be rather slow on large sets of terms. On the other hand, DDs have demonstrated their efficiency for model-checking, but translating a system semantics into efficient DDs operations is an expert’s matter. StrataGEM describes the semantics of a system in terms of strategies over a TR system, and automatically trans- lates these rules into operations on DD to handle the model-checking. The ultimate goal of StrataGEM is to become a verification framework for the different variants of Petri nets by separating the semantics of the model from the computation that performs model-checking.

Refereed DesignationRefereed