Introduction
The most widely used software verification techniques are peer reviewing and testing. In case of concurrent systems, these techniques can cover only a limited portion of possible behaviours. Formal methods can be used to establish a concurrent system correctness with mathematical rigour.
Model checking is one of the most promising techniques for automatic software analysis and Petri nets are one of the most widespread formalisms used in software engineering. Unfortunately, software tools for Petri nets are rarely equipped with model checking algorithms.
PetriNet2ModelChecker was designed to face this problem. It is an intuitive tool which core features enable translation of pupular classes of Petri Nets (P/T-, CP- and RTCP-nets) reachability graphs into the nuXmv language and Aldebaran format. As a result, the tool provides for the automatic model checking of nets created in the TINA and CPN Tools environments. The presented solution provides the possibility of formal verification of Petri nets designed with these environments using model checking techniques and mainstream model checkers - nuXmv for LTL and CTL temporal logics, CADP Evaluator for regular alternation-free mu-calculus.
PetriNet2ModelChecker integrates cpn2rtcpn and RTCPNC software and allows to load RTCP nets modelled in CPN Tools and generate their coverability graphs or simulators.