StrataGEM: A Generic Petri Net Verification Framework
In this paperwe 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 Rewriting (TR) to the efficiency of Decision Diagrams (DDs). TR systems are a great way to describe the semantics of a system, being readable and compact, 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 translates 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.
KeywordsCluster Detection Symbolic Model Check Term Rewrite System Term Rewrite Verification Framework
Unable to display preview. Download preview PDF.
- 3.Wolper, P., Godefroid, P.: Partial-Order Methods for Temporal Verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 233–246. Springer, Heidelberg (1993)Google Scholar
- 4.Buchs, D., Hostettler, S.: Sigma Decision Diagrams. In: Corradini, A. (ed.) TERMGRAPH 2009: Preliminary Proceedings of the 5th International Workshop on Computing with Terms and Graphs. Number TR-09-05 in TERMGRAPH Workshops, Università di Pisa, pp. 18–32 (2009)Google Scholar
- 9.International Organization for Standardization: ISO/IEC. Software and Systems Engineering - High-Level Petri Nets, Part 1: Concepts, Definitions and Graphical Notation. International Standard ISO/IEC 15909 (December 2004)Google Scholar
- 10.MoVe Team: GAL, http://move.lip6.fr/software/DDD/gal.php
- 12.Kordon, F., Buchs, D.: Model Checking Contest Page, http://mcc.lip6.fr/
- 13.MoVe Team: The PNXDD Home Page (2013), https://srcdev.lip6.fr/trac/research/NEOPPOD/wiki/pnxdd