=Paper=
{{Paper
|id=None
|storemode=property
|title=Distributed Verification of Modular Systems
|pdfUrl=https://ceur-ws.org/Vol-726/03-componet-1.pdf
|volume=Vol-726
}}
==Distributed Verification of Modular Systems
==
https://ceur-ws.org/Vol-726/03-componet-1.pdf
Proceedings of CompoNet and SUMo 2011
Distributed Verification of Modular Systems
M.C. Boukala1 and L. Petrucci2
1
LSI, Computer Science department, USTHB
BP 32 El-Alia Algiers, ALGERIA
boukala@lsi-usthb.dz
2
LIPN, CNRS UMR 7030, Université Paris XIII
99, avenue Jean-Baptiste Clément
F-93430 Villetaneuse, FRANCE
Laure.Petrucci@lipn.univ-paris13.fr
Abstract. The use of distributed or parallel processing gained interest
in the recent years to fight the state space explosion problem. Many in-
dustrial systems are described with large models, and the state space
being even larger, it does not fit completely into the memory of a single
computer.
To avoid the high space requirement, several reduction techniques have
been proposed: modular verification, partial order reductions, symme-
tries, using symbolic or compact representations like BDDs.
Another way to alleviate the state space explosion problem is to use
modular analysis, which takes advantage of the modular structure of a
system specification, particularly for systems where the modules exhibit
strong cohesion and weak coupling.
In this paper, we propose to combine distributed processing and modu-
lar analysis to perform verification of basic behavioural properties such
as reachability, deadlock states, liveness, and home states and their dis-
tributed analysis for modular systems. Each module is assigned to a
process which explores independently the internal activity of the mod-
ule, allowing a significant reduction in the size of the state space rather
than in an interleaved fashion.
Keywords: Modular systems, distributed verification, modular analysis,
Petri nets.
1 Introduction
Systems developed nowadays are both more and more complex and critical.
When addressing the design of such systems, it is necessary to ensure reliability,
by verifying the system properties. The main approach to verification consists
in the generation and analysis of the state space. Some properties such as reach-
ability or deadlocks can be verified on-the-fly, and only require information on
states reachable from the initial marking. On the contrary, liveness and home
states are elaborate properties which require a full generation of the state space
including not only nodes but also arcs. Even for small models, the size of the
state space may be too huge to fit in the memory of a single computer.
1
Proceedings of CompoNet and SUMo 2011
To cope with the state space explosion problem, several reduction techniques
have been proposed: on-the-fly verification checks properties during the state
space construction; sweep-line construction [Sch04] considers a progress mea-
sure, and discards states that will not be encountered further in the construc-
tion; modular verification [LP04]; partial order reductions [Val92,NG97]; sym-
metries [AHI98,CFJ93]; using symbolic or compact representations like BDDs
and Kronecker algebra.
Recently, several studies addressed distributed verification, many of them
focussing on distributed LTL model-checking [BBS01,BO03,LS99,BP07]. These
works are mainly based on the partionning of the state space.
The performances of distributed verification depends on several criteria, e.g.
load balancing of the partitioned state space, but also, more importantly, on
a good partitioning. Therefore, choosing an adequate hash function to assign
nodes to processors is important.
In [LP04] the modular analysis approach examines in isolation the local be-
haviour of each subsystem, and then separately considers the synchronisation
between the subsystems. In this fashion, exploring the many possible interleav-
ings of activity of the subsystems is avoided, thus reducing the state space.
In this work, we propose to combine modular analysis and distributed pro-
cessing to improve consequently the systems verification. We focus on checking
usual properties such as reachability, liveness and home states.
The paper is organised as follows. We assume the reader is familiar with basic
Petri nets notions. Hence, we recall in Section 2 only the modular concepts, i.e.
Modular Petri nets and Modular State Spaces. In section 3, we introduce algo-
rithms based on distributed modular construction of the state space. In section 4
distributed verification of various properties is presented. These algorithms have
been implemented in a prototype tool and experimental results are presented in
section 5. Finally, section 6 concludes the paper.
2 Modular Petri Nets
In this paper, we consider only modules synchronised through shared transitions
as in [LP04].
2.1 Definition of Modular Petri Nets
Definition 1 (Modular Petri net). A modular Petri net is a pair MN =
(S, TF ), satisfying:
1. S is a finite set of modules such that:
– Each module, s ∈ S, is a Petri net: s = (Ps , Ts , Ws , M0s ).
– The sets of nodes corresponding to different modules are pair-wise dis-
joint:
∀s1 , s2 ∈ S : [s1 6= s2 ⇒ (Ps1 ∪ Ts1 ) ∩ (Ps2 ∪ Ts2 ) = ∅].
2
Proceedings of CompoNet and SUMo 2011
S S
– P = Ps and T = Ts are the sets of all places and all transitions
s∈S s∈S
of all modules.
2. TF ⊆ 2T is a finite set of non-empty transition fusion sets.
S
In the following, TF also denotes tf ∈TF tf . We now introduce transition
groups.
Definition 2 (transition group). A transition group tg ⊆ T consists of either
a single non-fused transition t ∈ T \ TF or all members of a transition fusion
set tf ∈ TF .
The set of transition groups is denoted by TG.
A transition can be a member of several transition groups as it can be syn-
chronised with different transitions (a sub-action of several more complex ac-
tions). Hence, a transition group corresponds to a synchronised action. Note
that all transition groups have at least one element.
Next, we extend the arc weight function W to transition groups, i.e. ∀p ∈
P, ∀tg ∈ TG :
P P
W (p, tg) = W (p, t), W (tg, p) = W (t, p).
t∈tg t∈tg
Markings of modular Petri nets are defined as markings of Petri nets, over the
set P of all places of all modules. The restriction of a marking M to a module
s is denoted by Ms . The enabling and occurrence rules of a modular Petri net
can now be expressed.
Definition 3 (Transition group enabledness). A transition group tg is en-
abled in a marking M , denoted by M [tgi, iff:
∀p ∈ P : W (p, tg) 6 M (p)
When a transition group tg is enabled in a marking M1 , it may occur, changing
the marking M1 to another marking M2 , defined by:
∀p ∈ P : M2 (p) = (M1 (p) − W (p, tg)) + W (tg, p).
Figure 1 depicts a modular Petri net consisting of three modules A, B and
C. Modules A and B both contain transitions labelled F1 and F3 , while modules
B and C both contain transition F2 . These matched transitions are assumed to
form three transitions fusion sets.
Example: The (full) state space for the modular Petri net of figure 1 is shown
in figure 2. Note that the initial state is shown as A1 B1 C1 , thus indicating that
place A1 is marked with a token in module A, place B1 is marked with a token
in module B, and place C1 is marked with a token in module C. In this initial
state, only transition F1 is enabled, its occurrence leading to state A2 B2 C1 .
When considering the modular state space, as well as checking properties of
the system, we will use Strongly Connected Components. The set of all strongly
connected components is denoted by SCC. For a node v and a component c ∈
SCC we use v ∈ c to denote that v is one of the nodes in c. A similar notation
is used for arcs. We use v c to denote the component to which v belongs.
3
Proceedings of CompoNet and SUMo 2011
A1 B1 C1
F1 F1 F2
tB
A2 B2 C2
F3 F2 tA
A3
B3
F3
Fig. 1: A modular Petri net with 3 modules
2.2 Modular State Spaces
In the definition of modular state spaces, we denote the set of states reachable
from M by occurrences of local (non-fused) transitions only, in all the individual
modules, by [[M i.
The notation with a subscript s means the restriction to module s, e.g. [M is
is the set of all nodes reachable from the global marking M by occurrences of
transitions in module s only.
We use M [[σiiM 0 to denote that M 0 is reachable from M by a sequence
σ ∈ (T \ T F )∗ T F of internal transitions followed by a fused transition. In the
definition of modular state spaces we need a compact notation to capture the
states reachable from M in all the individual modules. It turns out that we can
use a product of SCCs of the individual modules to express this representative
node: for any reachable marking M , we use M c to denote the product (or tuple)
of Strongly Connected Components (SCCs) Msc of the individual modules:
Y
∀M ∈ [M0 i : M c = Msc .
s∈S
The definition of a modular state space consists of two parts: the state spaces of
the individual modules and the synchronisation graph.
Definition 4 (Modular state space). Let MN = (S, TF ) be a modular Petri
net with the initial marking M0 . The modular state space of MN is a pair
MSS = ((SS s )s∈S , SG), where:
1. SS s = (Vs , S
As ) is the local state space of module s:
(a) Vs = [vis
v∈VSG
4
Proceedings of CompoNet and SUMo 2011
A1 B1 C1
F1
A2 B2 C1 tB
F2 tA
A2 B3 C2 A3 B2 C1 tB
tA
F3 F2
A3 B3 C2
Fig. 2: The state space of the modular net of figure 1
(b) As = {(M1 , t, M2 ) ∈ Vs × (T \ TF )s × Vs | M1 [tiM2 }
2. SG = (VSG , ASG ) is the synchronisation graph of MN :
(a) VSG = [[M0 iic ∪ M0 0
c
0
(b) ASG = {(M1 , (M1 , tf ), M2c ) ∈ VSG × ([M0 ic × TF ) × VSG | M1 ∈ [[M1 i ∧
c c
0
M1 [tf iM2 }
A detailed explanation of the definition is given in [LP04]:
(1) The definition of the state space graphs of the modules is a generalization of
the usual definition of state spaces.
(1a) The set of nodes of the state space graph of a module contains all states
locally reachable from any node of the synchronisation graph.
(1b) Likewise the arcs of the state space graph of a module correspond to all
enabled internal transitions of the module.
(2) Each node of the synchronisation graph is labelled by a M c and is a repre-
sentative for all the nodes reachable from M by occurrences of local transitions
only, i.e. [[M i. The synchronisation graph contains the information on the nodes
reachable by occurrences of fused transitions.
(2a) The nodes of the synchronisation graph represent all markings reachable
from another marking by a sequence of internal transitions followed by a fused
transition. The initial node is also represented.
(2b) The arcs of the synchronisation graph represent all occurrences of fused
transitions.
The state space graphs of the modules contain only local information, i.e.
the markings of the module and the arcs corresponding to local transitions but
not the arcs corresponding to fused transitions. All the information concerning
these is stored in the synchronisation graph.
The nodes of the synchronisation graph represent all markings reachable
from another marking by a sequence of internal transitions followed by a fused
transition. The initial node is also represented.
5
Proceedings of CompoNet and SUMo 2011
The arcs of the synchronisation graph represent all occurrences of fused tran-
sitions. Each arc is labelled by the corresponding fired transition and by the
SCCs of the markings which enabled this transition. But only the SCCs of the
participating modules do appear.
Example: The modular state space for the modular Petri net of figure 1 is shown
in figure 3. Note that there is a local state space for each module, as well as a
synchronisation graph which captures the occurrence of fused transitions. We do
not distinguish between nodes and SCCs since, in this case, all SCCs consist of
a single node (which is seldom the case in practice).
Module A Module B Module C Synch. Graph
A1 B1 C1 A1 B1 C1
A1 B1 C1 , F1
A2 B2 tB C2 A2 B2 C1
tA A2 B2 C1 , F2
A3 B3 A2 B3 C2 A3 B3 C2 , F3
Fig. 3: The modular state space of the net in figure 1
Although sketches of algorithms were introduced in [LP04], we give here the
description of the distributed algorithms for the construction of the state space
and for the verification of the reachability, dead markings, liveness, and home
states properties.
3 Distributed Construction of the Modular State Space
Several works have developed distributed tools generating and exploring the
state space on a cluster of workstations. Partitioning the set of states over the
different stations is done using a hash function [GMS01,KP04,AAC87,LP04].
This approach can handle larger state spaces but still remains limited.
Here, we consider a different approach based on modularity to achieve a dis-
tributed construction of the state space and the verification of various properties.
In this approach we also used two types of processes. They consist in a
coordinator process and N worker processes, one worker process for each module,
as in [KP04].
6
Proceedings of CompoNet and SUMo 2011
The coordinator constructs the synchronisation graph, coordinates the differ-
ent worker processes and determines the termination of the modular state space
construction, while every worker generates the local state space of the module
it is assigned by firing only internal transitions.
The coordinator process starts by sending the initial marking M0s restricted
to module s to each worker process, and waits for receiving the states enabling
fused transitions from the workers processes.
Algorithm 1: Internal State Space Generation()
1 begin
/* Process states in Waiting */
2 while ¬EndOfGeneration do
3 while Waiting 6= ∅ do
4 Choose M ∈ Waiting s
5 forall the t 6∈ TF s.t. M [tiM 0 do
/* t is an enabled internal transition */
6 Add (M 0 )
7 Arc (M, t, M 0 )
8 UpdateSCC ()
9 forall the tf ∈ TF s.t. M [tf i do
/* M enables a fused transition tf */
10 TFWaiting ← TFWaiting ∪ {(M, tf )};
11 Waiting s ← Waiting s \ {M }
12 if TFWaiting = ∅ then
13 EndOfGeneration = true
14 else
15 while TFWaiting 6= ∅ do
16 Choose (M, tf ) ∈ TFWaiting s.t. M [tf iM 0
17 Waiting s ← Waiting s ∪ {M 0 }
18 TW .label = M c
19 TW .AncSCC = AncSCC (M )
20 TW .tr = tf
21 TW .SuccSCC = M 0c
22 Send (Sender = s, Dest = Coordinator, Type = SynchTrans,
23 Content = TW )
24 Send (Sender = s, Dest = Coordinator, Type = END_GENERATION)
25 end
When a worker process s receives the initial marking, it adds it to the sets
Vs and W aitings , that correspond respectively to the set of local markings and
the set of markings which are visited but not explored yet. The worker process
then invokes algorithm 1 to generate the internal state space of the module it is
7
Proceedings of CompoNet and SUMo 2011
assigned. Function Add (M ) adds the marking M to both sets Vs and W aitings
if it is not already in Vs .
The workers send enabled fused transitions to the coordinator process. Actu-
ally, the message sent to the coordinator not only contains the fused transition tf
but also the SCC number M c of the marking enabling tf , and the SCC number
of its predecessor marking in the synchronisation graph (in a field AncSCC ).
The communications are asynchronous. Thus, when receiving a message,
the coordinator and worker processes are preempted and a handler function
MessageHandler() is invoked. Algorithm 2 describes the actions performed by
the coordinator when it receives a fused transition from the worker process s.
The parts handling other messages are not detailed. They concern the algo-
rithm termination (and is similar to the termination in [KP04]), as well as the
analysis messages introduced in section 4.
First, the coordinator creates the initial node v0 = M0c ∈ VSG . When a
fused transition tf is received from a process s, the successors of a node v =
(v1 , v2 , . . . vN ) ∈ VSG are computed as follows:
– we consider the set PM of the modules (processes) participating in the syn-
chronisation of the fused transition tf ;
– we construct the sets:
• Wpm corresponding to the fused transition tf received earlier from other
processes;
• Ws corresponding to the fused transition received from process s;
• Wnp contains • for modules not participating in the synchronisation;
– for all possible combinations, the successor nodes in the synchronisation
graph are calculated.
The successor states thus computed are sent to the worker processes for an
additional round of internal state space generation.
4 Properties
A major issue is the analysis of concurrent systems properties. The reachabil-
ity graph is the basic model on which most verifications are built. Behavioural
properties, which depend on initial marking, and the reachability graph are often
used to perform such analysis.
In this work we focus on basic behavioural properties: reachability, deadlocks,
liveness, home state and their distributed analysis.
4.1 Reachability
The reachability problem for Petri nets consists in proving that a given marking
M is in [M0 i. This property is often used to check whether a faulty state M
is reachable, e.g. an elevator moving while the door is open. It is convenient to
look for erroneous states.
8
Proceedings of CompoNet and SUMo 2011
Algorithm 2: Message Handler()
1 begin
..
.
2 if Message.Type = SynchTrans then
/* message received contains an enabled fused transition */
3 tf = Message.Content.tr
4 s = Message.Sender
5 PM = {i s.t. tf ∈ Ti }
/* PM: modules participating in the synchronisation of tf */
6 foreach v = (v1c , v2c , · · · , vN
c
) ∈ VSG do
7 foreach pm ∈ PM and pm 6= s do
8 Wpm = {w ∈ SGWaiting pm s.t.
c
9 (w.AncSCC = vpm ) ∧ (w.tr = tf )}
/* Wpm : markings enabling tf , with vpm as ancestor */
10 foreach np 6∈ PM and np 6= s do
11 Wnp = {•}
/* any marking of a non-participating module enables
synchronisation */
12 Ws = {Message.Content}
13 foreach C = (c1 , c2 , · · · , cN ) s.t. ∀i ∈ PM , ci ∈ Wi do
c c c
14 v 0 = (v 0 1 , v 0 2 , · · · , v 0 N ) where:
c c
15 ∀i ∈ PM , v 0 i = ci .SuccSCC and ∀i 6∈ PM , v 0 i = vic
0
16 Add (v )
17 AddArc (v, (C , ft), v 0 )
18 foreach pm ∈ PM do
19 Send (Sender = Coordinator, Dest = pm, Type = NEW_NODE,
0
20 Content = vpm )
21 SGWaiting s = SGWaiting s ∪ Message.Content
..
.
22 end
9
Proceedings of CompoNet and SUMo 2011
In some applications, one may be interested in the markings of a subset of
places and not care about the others places in the net. This leads to a submarking
reachability problem.
Reachability is known to be decidable. For modular systems, determining
whether a given state M is reachable from the initial marking can be done in
a parallel way: each worker process s searches through its local state space Vs .
Then, if one of the worker processes does not find Ms in its local state space
Vs , marking M is not reachable. Otherwise i.e. (∀s ∈ {1..N } Ms ∈ Vs ), all
the workers send the ancestor SCCs of Ms to the coordinator. The coordinator
stores the SCCs received from each worker s and checks whether there exists a
combination of these in the set of nodes of the synchronisation graph VSG .
4.2 Deadlocks
The algorithm used to find dead markings in a modular state space is based on
the following proposition:
Proposition 1 (Deadlocks).
M ∈ [M0 i is a deadlock ⇔ [ ∀s ∈ S : (M s)c ∈ T erm(SCCs ) ∩ T rivial(SCCs ))
∧(∀(v1 , (M1c , tf ), v2 ) ∈ ASG : M1c 6= M c )]
Each worker process s searches in its local state space for the local dead
markings which consist in trivial terminal SCCs. If there exists a worker process
without such a node, the module assigned to this worker always allows a local
behaviour. Hence, the system is deadlock-free. Otherwise, every worker process
sends the SCCs corresponding to the locally dead markings to the coordinator
process.
The coordinator process stores the SCCs received from the workers. It then
checks each combination of such markings: if it labels an arc in the synchroni-
sation graph, the corresponding fused transition is enabled and the marking is
not a deadlock. Otherwise, if the marking is effectively reachable, then it is a
deadlock.
4.3 Liveness
To verify whether a transition t is live or not, two cases are distinguished: if t
is a fused transition (t ∈ TF ), or t is an internal transition. The verification is
based on the following proposition.
Proposition 2 (Liveness).
1. A transition tf ∈ TF is live ⇔
[∀scc ∈ Term(SCCSG ) : tf ∈ Trans(scc)]
∧ [∀v ∈ VSG : ∀M ∈ [[vi :(∀s ∈ S : Msc ∈ Term(SCCs ))
⇒ ∃(v, (M1 , tf 0 ), v2 ) ∈ ASG : M1 ∈ [[M i].
10
Proceedings of CompoNet and SUMo 2011
2. A transition t ∈ Ts is live ⇔
[∀scc ∈ Term(SCCSG ) : ∃v ∈ scc : t ∈ Trans([vs is )]
∧ [∀v ∈ VSG : ∀M ∈ [[vi : (Msc ∈ Term(SCCs ))
⇒ (t ∈ T rans(Msc ) ∨ ∃(v, (M1 , tf ), v2 ) ∈ ASG : M1 ∈ [[M i))].
To check if a fused transition tf is live, the coordinator checks if there exists
a terminal SCC in the synchronisation graph which does not contain transition
tf , in which case transition tf is not live. Otherwise, for each node v ∈ VSG
of the synchronisation graph, the coordinator sends vs to the worker process s
and waits to receive the terminal SCCs reachable from vs in module s. Then,
it checks whether the combinations of the terminal SCCs label fused transitions
are in SG, considering only the modules participating in the synchronisation of
this fused transition. If this is not the case, tf is not live.
When transition t is an internal transition of module s, the worker process s
detects the terminal SCCs which do not enable t, that may invalidate liveness.
For each node v ∈ VSG of the synchronisation graph, the coordinator sends vs
to the worker process s. The worker processes check whether these problematic
SCCs are reachable from vs , and send them to the coordinator. The coordinator
checks if there exists a combination that does not label a fused transition, in
which case transition t is not live.
4.4 Home States
The verification of whether a reachable state MH is a home state or not is based
on the following proposition.
Proposition 3 (Home state).
A state MH ∈ [M0 i is a home state ⇔
[∀scc ∈ Term(SCCSG ) : ∃v ∈ scc : MH ∈ [[vi]
∧ [∀v ∈ VSG : ∀M ∈ [[vi : (∀s ∈ S : Msc ∈ Term(SCCs ))
⇒ MH ∈ [[M i ∨ ∃(v, (M1 , tf , M2 ), v2 ) ∈ ASG : M1 ∈ [[M i].
To check such a property, we first check whether the state MH is reachable
from all nodes of the synchronisation graph. Then, for every node v of the syn-
chronisation graph, the coordinator asks the worker processes for the terminal
SCCs reachable from v by firing internal transitions only. The coordinator checks
then that all combinations label an arc, or correspond to the SCC containing
MH . Otherwise MH is not a home state.
5 Implementation and experiments
The previous algorithms were implemented within a prototype tool. The tests
were carried on a cluster composed of 12 stations (Pentium IV with 512 Mbytes
of memory), one of them is assigned to the coordinator process while the others
run the worker processes.
In this section, we give the results obtained for the dining philosophers prob-
lem and Automated Guided Vehicles (AGV) problem, and draw conclusions.
11
Proceedings of CompoNet and SUMo 2011
5.1 The dining philosophers problem
The distributed generation based on partitioning the state space over a cluster
of stations, allows for handling large size problems. In [BP07], the philosophers
problem was handled with various sizes (see Table 1).
Nb Philo Nb States Nb Trans Nb Cross. arcs Nb Mess. CPU Time (sec)
5 11 30 18 36 <0.01
10 123 680 242 494 <0.01
15 1,364 11,310 2,731 5477 0.06
20 15,127 167,240 30,236 60,493 2.52
25 167,761 2,318,400 315,718 631,587 32.58
30 1,728,813 28,686,031 3,572,821 7,156,116 7547.45
Table 1: Distributed generation based on partitioning the state space
But this approach is still limited. The total number of exchanged messages
is very high, due to the amount of cross arcs.
In the distributed modular based approach, the original Petri net is split into
a Modular Petri net with N modules and each module, which can contain m
philosophers, is assigned to a worker process. Philosopher i of module l shares its
forks with the philosophers i − 1 and i + 1 of the same module for 2 ≤ i ≤ m − 1.
Philosophers 1 in module l and m in module (l − 1) mod N + 1 also share a fork.
The nature of the Petri net gives 4 SCCs in each module graph. The syn-
chronisation graph size is 2N nodes and N.2N arcs. For a problem with 100
philosophers, if we consider 10 modules with 10 philosophers each, we obtain
1,024 nodes and 10,240 arcs in the synchronisation graph, 233 nodes and 1,132
arcs in each local graph. The reachability graph size for the original problem is
greater than 7 × 1020 nodes and 7 × 1022 arcs.
In Table 2, we give the modular state space sizes for the philosophers problem
considering 10 philosophers per module each time. The average of CPU times of
the coordinator is also given.
Nb Philo Nodes N Arcs Mess Nb CPU Time (sec) CPU time (1 proc)
20 470 2162 26 0.04 0.08
40 948 4372 52 0.04 0.16
60 1462 6846 84 0.04 0.25
80 2120 10664 120 0.05 0.39
100 3354 21010 230 0.16 0.61
Table 2: Modular distributed generation
The CPU time of the workers is generally equal to 0.04 s (for 10 philosophers
per module). Thus, in the first cases the global CPU time corresponds to the
12
Proceedings of CompoNet and SUMo 2011
local state space generation, the synchronisation graph generation CPU time is
less then 0.01 s. In the last cases the synchronisation graph generation spends
more time since its size became larger.
Various tests were performed for reachability, liveness and home state prop-
erties, with the philosophers problem of 10 modules with 10 philosophers in each
one, the experimental results are given in the table 3.
Properties CPU Time (sec) Mess Nb
Reachability1 < 0.01 20
Reachability2 0.03 20
Reachability3 0.02 20
Liveness (Internal tr) 0.17 4278
Liveness (F uzed tr) 0.15 4116
Home state 0.21 4432
Table 3: Distributed modular verification of properties of the philosophers example
For reachability, we considered three cases: in the first, the marking is not
reachable in some modules; in the second, the marking is reachable in the mod-
ules but not reachable as a global marking; and in the third case, the marking
is reachable. The number of exchanged messages is the same and correspond to
messages sent by the coordinator to the worker processes to transmit the mark-
ing to check (10 messages) and to the answers of the workers (10 messages).
The liveness and home state verifications are performed with a relatively large
number of exchanged messages: since all transitions are live, the coordinator
must obtain the terminal SCCs reachable from each node of the synchronisation
graph. When the coordinator moves from a node to its successor in the synchro-
nisation graph, it transmits messages only to the workers corresponding to the
changed components to have their terminal SCCs. This allows for minimising
the number of messages transmitted by the coordinator.
5.2 Automated Guided Vehicles
The Automated Guided Vehicles (AGVs) problem has been solved by means of
Modular State Spaces in [LP04]. The problem is that of a factory floor which
consists of three workstations which operate on parts, two input and one output
stations, and five AGVs which move parts from one station to another.
The 5 AGVs example is loosely coupled. Therefore, much interleaving is
avoided when building the modular state space and this leads to very good
results. This model has 30,965,760 states (see [LP04]). However, with modu-
lar analysis we obtain only 900 states with 2,687 arcs. The analysis based on
modular distribution gives also good results as shown in table 4.
13
Proceedings of CompoNet and SUMo 2011
CPU Time (sec) Mess Nb
State Space Generation 0.02 82
Deadlocks search 0.03 11
Reachability1 < 0.01 22
Reachability2 0.02 22
Reachability3 0.02 22
Liveness (Internal tr) 0.09 3313
Liveness (F uzed tr) 0.08 3062
Home state 0.15 3415
Table 4: Distributed verification of properties for the 5 AGVs example
6 Conclusion
In this paper, we proposed steps towards distributed modular analysis of Petri
net models, based on the construction framework of [LP04]. Using these algo-
rithms, it is possible to verify standard Petri nets properties, such as reachability,
deadlocks, home states and liveness, in a distributed manner.
The main advantage of such an approach is the possibility to consider very
large systems with several modules, sharing transitions, and assign them among a
set of machines, thus limiting the drawbacks of the state space explosion problem.
Each machine (process) generates only the state space of the module it is
assigned. The synchronisation graph provides the global knowledge of the be-
haviour of the system.
Moreover, it is also possible to check properties using the distributed modu-
lar state space directly, i.e. without unfolding to the ordinary state space. When
designing algorithms there is often a trade-off between time and space complex-
ity. For state space analysis it is attractive to have a rather fast way to decide
properties, but the state space explosion problem makes it absolutely necessary
to minimise memory usage.
Experiments were performed on a cluster of 12 stations. Both the AGVs,
and the philosophers problems were considered, with different sizes. The results
obtained for the generation of the modular state space were very interesting
and allow for checking properties of very large systems. Future work will ex-
tend properties verification to temporal logic properties. Further experiments
on larger case studies are also necessary for a better assessment of the benefits
of this approach.
References
[AAC87] S. Aggarwal, R. Alonso, and C. Courcoubetis. Distributed reachability anal-
ysis for protocol verification environments. In P. Varaiya and H. Kurzhan-
ski, editors, Discrete Event Systems: Models and Application, volume 103 of
LNCIS, pages 40–56. Springer-Verlag, 1987.
14
Proceedings of CompoNet and SUMo 2011
[AHI98] K. Ajami, S. Haddad, and J.-M. Ilié. Exploiting symmetry in linear temporal
model checking: One step beyond. In Proc. 4th Int. Conf. Tools and Algo-
rithms for the Construction and Analysis of Systems (TACAS’98), volume
1384 of Lecture Notes in Computer Science, pages 52–67, 1998.
[BBS01] J. Barnat, L. Brim, and J. Strîbrnà. Distributed LTL model checking in
SPIN. In Proc. 8th International SPIN workshop on Model Checking Software
(SPIN’2001), volume 2057 of Lecture Notes in Computer Science, pages 200–
216. Springer-Verlag, 2001.
[BO03] S. Blom and S. Orzan. Distributed state space minimization. Electronic Notes
in Theoretical Computer Science, 80:1–15, 2003.
[BP07] M.C. Boukala and L. Petrucci. Towards distributed verification of Petri nets
properties. In British Computer Society eWIC, editor, In Proc. 1st Interna-
tional Workshop on Verification and Evaluation of Computer and Communi-
cation Systems (VECOS’07), Algiers, Algeria, pages 15–26, 2007.
[CFJ93] E. M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal
logic model checking. In Proc. 5th Int. Conf. Computer Aided Verification
(CAV’93), volume 697 of Lecture Notes in Computer Science, pages 450–462.
Springer-Verlag, 1993.
[GMS01] H. Garavel, R. Mateescu, and I. Smarandache. Parallel state space construc-
tion for model-checking. In Proc. 8th International SPIN workshop on Model
Checking Software (SPIN’2001), volume 2057 of Lecture Notes in Computer
Science, pages 217–234. Springer-Verlag, 2001.
[KP04] L. Kristensen and L. Petrucci. An approach to distributed state exploration
for coloured Petri nets. In Proc. 25th Int. Application and Theory of Petri
Nets (ICATPN’2004), volume 3099 of Lecture Notes in Computer Science,
pages 474–483. Springer-Verlag, 2004.
[LP04] C. Lakos and L. Petrucci. Modular analysis of systems composed of semiau-
tonomous subsystems. In In Proc. 4th Int. Conf. on Application of Concur-
rency to System Design (ACSD’2004), Hamilton, Canada., pages 185–194.
IEEE Computer Society Press, 2004.
[LS99] F. Lerda and R. Sisto. Distributed-memory model checking with SPIN. In
Proc. 5th and 6th International SPIN workshops on Model Checking Software
(SPIN’1999), volume 1680 of Lecture Notes in Computer Science, pages 22–
39. Springer-Verlag, 1999.
[NG97] R. Nalumasu and G. Gopalakrishnan. A new partial order reduction al-
gorithm for concurrent systems. In Proc. Int. Conf. Hardware Description
Languages and their Applications (CHDL’97). Chapman & Hall, 1997.
[Sch04] K. Schmidt. Automated generation of a progress measure for the sweep-line
method. In Proc. 10th Int. Conf. Tools and Algorithms for the Construc-
tion and Analysis of Systems (TACAS’04), volume 2988 of Lecture Notes in
Computer Science, pages 192–204. Springer-Verlag, 2004.
[Val92] A. Valmari. A stubborn attack on state explosion. Formal Methods in Systems
Design, 1(4):297–322, 1992.
15
Proceedings of CompoNet and SUMo 2011
16