The paper deals with the problem of translation of reachability graphs for place-transition and coloured Petri nets into the NuSMV language. The translation algorithms presented in the paper have been implemented as a part of the PetriNet2NuSMV tool so the translation is made automatically. The PetriNet2NuSMV tool works with reachability graphs generated by the TINA and CPN Tools software. Thus, it provides the possibility of formal verification of Petri nets designed with these environments using model checking techniques and a mainstream model checker for LTL and CTL temporal logics.
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 [
There are some similar tools described in the literature such as PEP [
The aim of this work was to create a tool for translation of reachability graphs of both place-transition and coloured Petri nets into a description of the system in the
NuSMV language. As a result, the tool provides for the automatic model checking of nets created in the TINA and CPN Tools environments. The presented solution is the only one that allows verification of formulae in both LTL and CTL temporal logics for coloured Petri nets as well as for PT-nets.
The paper is organised as follows. Section 2 provides a short introduction to the NuSNV language and tool. Section 3 deals with reachability/coverability graphs for place-transition nets and the algorithm of transformation of such graphs into the NuSMV language. The algorithm of transformation of reachability graphs for coloured Petri nets into the NuSMV language is presented in Section 4. Section 5 provides some test results for the presented algorithms. A short summary is given in the final section. 2
NuSMV [
In the NuSMV approach, the verified system is modelled as a finite state transition
system [
MODULE main VAR s : {s0, s1, s2}; a : boolean; b : 0 .. 2; ASSIGN init(s) := {s0, s2}; next(s) := case s = s0 : s1; s = s1 : {s1, s2}; s = s2 : s2; esac; a := case s = s0 : TRUE; s = s2 : TRUE;
TRUE : FALSE; esac; b := case s = s0 : 1; s = s1 : 2;
TRUE : 0; esac; } set of states
atomic propositions given implicitly } initial states transition relation labelling function
NuSMV is equipped with a dedicated modelling language (the SMV language),
which is used to define finite state transition systems [
A finite state transition systems is stored as a text file. NuSMV statements LTLSPEC and CTLSPEC can be used to include LTL and CTL formulae respectively into the file. In case of the LTL logic, the temporal operators G (globally), F (finally), X (next), U (until) can be used. Moreover, the propositional logic operators are represented by: ! (not), & (and), | (or), xor (exclusive or), -> (implies) and <-> (equivalence). In case of CTL following temporal logic operators can be used: EG (exists globally), EX (exists next state), EF (exists finally), AG (forall globally), AX (forall next state), AF (forall finally), E[ U ] (exists until), A[ U ] (forall until). Satisfaction of each specified formula is verified with the NuSMV tool automatically. If a modelled system does not satisfy a given formula, a proper counterexample is presented. It is finally worth mentioning that NuSMV can verify systems of high complexity, i.e. containing more than 1020 states. These features make NuSMV useful and convenient tool for finite automata verification. 3
Place-transition nets (PT-nets) [
A state of a PT-net is called marking and is a distribution of tokens among places of the net. Tokens are indistinguishable one from another so a marking of a place is represented by the number of tokens stored in the place. If P = fp1; : : : ; png, then a marking M is represented by the vector M = (M (p1); : : : ; M (pn)). A firing of a transition may change the current marking. A transition t is enabled if each input place p of t contains at least W (p; t) tokens, where W (p; t) is the weight of the arc from p to t. A firing of an enabled transition t removes W (p; t) tokens from each input place p of t, and adds W (t; p) tokens to each output place p of t. We write M !t M 0 to indicate that a firing of a transition t transforms M to M 0.
A sequence of firings results in a sequence of markings. A marking M 0 is said to be reachable from a marking M if there exists a sequence of firings that transforms M to M 0, i.e. there exist markings M1; : : : ; Mn and transitions t1; : : : ; tn such that M t!1 M1 t!2 : : : t!n Mn = M 0. The firing sequence t1; : : : ; tn is said to be feasible from the marking M . The set of all markings reachable from a marking M is denoted by R(M ) and the set of all firing sequences feasible from M is denoted by L(M ).
A reachability graph of a PT-net N = (P; T; A; W; M0) is the directed graph G = (V; A), such that the set of nodes V = R(M0), and the set of arcs A = f(M; t; M 0) 2 V T V : M !t M 0g. The arcs are labelled with transition names and there may exist more than one arc between the same pair of nodes. An example of a PT-net and its reachability graph are shown in Fig. 2.
p0 2 t3 2
t0 t1 2 p1 t2 p2 t0
(2, 0, 0)M0 (1, 1, 0)M1
t0 t3 (0, 2, 0)M3 t1
t3 t2 (0, 1, 1)M5 (1, 0, 1)M4 t2 t2 t3 t0 (0, 0, 2)M2
Let us consider the PT-net from Fig. 2 but with W (t1; p2) = 3, W (p2; t3) =
W (t3; p0) = 2. In such a case the number of tokens in places of the net can grow
infinitely, so the reachability graph is infinite. Then, the coverability graph [
The approach presented in the paper uses TINA [
Kts files contain sections starting with the word state and the order number of the state it represents. There is one section for each node of the reachability graph. The second line of each section contains information about the state marking. In the given example, line props p0*2 indicates that there are two tokens in place p2 (M (p2) = 2) and other places are empty. The third line of a section describes the active transitions in the given state. For example, line trans t0/1 t1/2 means that there are two active transitions in the state – t0 and t1. The former leads to state s1, and the latter to state s2. The letter w denotes the infinity. If a coverability graph does not contain the infinity symbol, then the coverability and reachability graphs are identical.
The PetriNet2NuSMV tool parses an input kts file and generates the system model in the SMV language. To this end the tool uses the designed translation algorithm. The algorithm is presented in Figure 4. A fragment of the SMV file generated for reachability graph from Fig. 2 is given below.
Listing 1.1. A fragment of SMV file generated for reachability graph from Fig. 2.
. pi : 0..k; where 8pi2P;Mj2R(M0)Mj(pi) 6 k 1: add MODULE main statement 2: add VAR keyword 3: for all Mi 2 R(M0) do 4: add si to the set of states s 5: end for 6: for all pi 2 P do 7: if 8Mj2R(M0)Mj(pi) 6 1 then 8: add Boolean variable pi 9: else 10: add bounded Integer variable pi
Listing 1.2. Examples of LTL and CTL formulae for the model from Listing 1.1. CTLSPEC AG EF (p0 = 2 & p1 = 0 & p2 = 0) LTLSPEC G (p0 <= 2 & p1 <= 2 & p2 <= 2) LTLSPEC G (p0 + p1 + p2 = 2) LTLSPEC G (p0 = 2 -> X (p0 != 2)) CTLSPEC AG (p1 = 2 -> AX (EF (p1 = 2))) . s : {s0, s1, ...}; . pi : boolean;
Examples of LTL and CTL formulae for the model from Listing 1.1 are shown in Listing 1.2. For example, the first one denotes that the corresponding PT-net is reversible, the second one denotes that the net is 2-bounded, the third denotes that the net is conservative etc. It is easy to check that all these formulae hold for the model. It is not so obvious if a reachability graph contains thousands of nodes and arcs. 4
Coloured Petri nets (CP-nets) combines the capabilities of PT nets with the capabilities
of a high-level programming language [
A non-hierarchical CP-net is a nine-tuple N = (P; T; A; ; V; C; G; E; I ), where P , T and A have meaning as for PT-nets, is a finite set of non-empty colour sets (types of tokens), V is a finite set of variables of types from , C : P ! is a colour set function that assigns to each place the type of its tokens; G is a guard function that assigns a guard (Boolean condition) to each transition (the default value is true); E is an arc expression function that assigns to each arc an expression that evaluates to a multi-set of tokens of the type assigned to the arc place node; and I is an initialization function that assigns to each place an expression that evaluates to a multi-set of tokens of the type assigned to the place.
A marking of a place p 2 P of a CP-net is multi-set of tokens of type C(p) 2
[
Sets R(M ) and L(M ) are defined as for PT-nets, but binding elements are taken into consideration instead of transitions. A reachability graph of a CP-net has a node for each reachable marking and an arc for each occurring binding element. An example of a CP-net is presented in Fig. 5. Its reachability graph is shown in Fig. 6.
For an effective modelling CP-nets enable to distribute parts of the net across
multiple subnets called modules. The result of such an approach is a hierarchical CP-net [
The most popular software for CP-nets modelling and reachability graphs
generation is CPN Tools [
(x,y,p) 1`2++3`7
p0 I
It is a powerful and efficient tool for editing, simulation and analysis of coloured Petri nets. CPN Tools provides for the automatic reachability graph generation by taking advantage of its state space toolbox. In order to do this, few steps are required. The first step is to make use of Calculate state space feature followed by Calculate SCC graph operation. To actually generate nodes and arcs of a reachability graph, Display partial state space feature must be called on auxiliary text element containing short ML code: EvalAllArcs(fn arc => arc). Nodes in the list option must be unchecked for this feature to work properly. Generated graph is saved with the model in a cpn file. Parsing process of a cpn file is relatively simple due to its XML structure. After parsing of a cpn file, PetriNet2NuSMV tool generates SMV output. The translation algorithm for CP-nets is presented in Figure 7. Illustrative parts of the generated SMV file for the reachability graph from Fig. 6 are presented in Listing 1.3. 1: add MODULE main statement 2: add VAR keyword 3: for all Mi 2 R(M0) do 4: add si to the set of states s . s : {s0, s1, ...}; 5: end for 6: L = ; . the set of defined variables’ labels 7: for all pi 2 P do 8: for all colour cj 2 Mk(pi), where Mk 2 R(M0) do 9: create marking label ltemp by concatenating pi and cj 10: if @l2Ll = ltemp then 11: add bounded Integer variable l_temp
. l_temp : 0..k; where 8pi2P;Mj 2R(M0) jMj (pi)j 6 k
Listing 1.3. Selected fragments of SMV file generated for reachability graph from Fig. 6. MODULE main VAR s: {s1, s2, s3, s4, s5, s6, s7, s8, s9}; p0_7 : 0..3; ...
ASSIGN init(s) := s1; next(s) := case s = s1 : {s5, s4, s3, s2}; s = s2 : s6; ... esac; p0_7 := case s = s5 : 2; s = s1 : 3; s = s6 : 2; ...
TRUE : 0; esac;
In order to make this notation clear, the meaning of labels will be shortly explained. The value of p0_7 variable denotes the number of tokens of value 7 in place p0. Bearing this in mind, s = s5 : 2 denotes: There are 2 tokens of value 7 in place p_0 in state s5. 5
Along with the presented algorithm, fully functional tool called PetriNet2NuSMV has been developed. In accordance with original ideas this tool allows to translate both kts and cpn files into smv files. As a result, users can easily validate the modelled system using LTL and CTL temporal logic formulae.
In order to facilitate the usage of the tool it was developed with simple graphical user interface (see Fig. 8). It allows to configure the parser, load an input file and save the generated output to the smv file. The application is written in Java using Swing library so it can serve both Linux and Windows users.
A summary of translation results for illustrative systems modelled in Tina and CPN Tools is presented in Table 1. The table contains translation times for four Petri net models with varying complexity and size of their reachability graphs. The measured times proved to be entirely satisfactory. NuSMV code is generated visibly faster for PT-nets. Nonetheless, even complex graph of CP-net model consisting of more than 2000 nodes and 20 000 arcs is translated in approximately 20 seconds. Considering the large size of the CPN Tools file that needs to be parsed, which is more then 20 MB, the result can be considered as adequate. Manual approach to NuSMV code creation for the mentioned Petri net model is practically impossible. 6
Algorithm for translation of reachability graphs for place-transition and coloured Petri nets into the NuSMV language has been presented in the paper. Both of these algorithms have been implemented as the core of PetriNet2NuSMV software. The tool has been tested against reachability graphs of different sizes and complexity and proved to be quite swift and efficient. PetriNet2NuSMV enables users to translate reachability graphs generated with TINA and CPN Tools environments into a NuSMV model automatically. Thus, a Petri model can be verified using model checking techniques without necessity of learning any additional language for the specification of requirements. Moreover, the presented algorithms for low and high level Petri nets can be adapt to other classes of Petri nets.