=Paper=
{{Paper
|id=Vol-1161/11610036
|storemode=property
|title=A High-Level Nets based Approach for Reconfigurations of Distributed Control Systems
|pdfUrl=https://ceur-ws.org/Vol-1161/11610036.pdf
|volume=Vol-1161
|dblpUrl=https://dblp.org/rec/conf/apn/KheldounZBI14
}}
==A High-Level Nets based Approach for Reconfigurations of Distributed Control Systems==
https://ceur-ws.org/Vol-1161/11610036.pdf
A high-level nets based approach for reconfigurations of
distributed control systems
Ahmed Kheldoun1 , JiaFeng Zhang2 , Kamel Barkaoui3 , and Malika Ioualalen4
1
Sciences and Technology Faculty, Yahia Fares University, Medea, Algeria
ahmedkheldoun@yahoo.fr
2
School of Electro-Mechanical Engineering, Xidian University, Xi’an 710071, China
zhangjiafeng628@gmail.com
3
CNAM, 292 Rue Saint-Martin 75141, Cedex 03 Paris, France
kamel.barkaoui@cnam.fr
4
MOVEP, Computer Science Department, USTHB, Algiers, Algeria
mioualalen@usthb.dz
Abstract. The paper deals with automatic reconfiguration problems of distributed
control systems that are composed of a group/set of networked reconfigurable
devices. A multi-agent architecture is proposed such that each device of a dis-
tributed control system has a special self-governed agent named reconfiguration
sub-controller agent to manage its local reconfiguration. Accordingly, a commu-
nication protocol is developed to handle interaction style among these agents for
the purpose of consistency. The proposed architecture is modeled by RECAT-
Nets and the distributed reconfiguration process is modeled by an ECATNet. Fur-
thermore, in order to check the correctness of the proposed approach, the model
checker Maude is applied, where required properties are specified by Linear Tem-
poral Logic. Finally, a virtual distributed control system contains two reconfig-
urable devices is applied to illustrate this work.
Keywords: Distributed control systems, Reconfiguration, Agent-based system, Recur-
sive ECATNet.
1 Introduction
Distributed reconfigurable control systems (DRCSs) receive more and more attention
from academic and industry for their broad application prospects [1],[2]. In industry, the
development of safe DRCSs is not an obvious activity because of their dynamic recon-
figurations that are implemented by the dynamic addition/removal of software/hardware
components, the modification of logic relationship among components, and the adjust-
ment of system states and data [3],[4]. This type of systems manages a set of networked
reconfigurable devices that should cooperate with each other, since any uncontrolled
automatic reconfiguration applied in a device may cause serious disturbance on others
and thus on the safety and correctness of the whole system.
Many researchers have tried to deal with the formal modeling of control systems
with potential reconfigurations. The author of [5] proposed self-modifying nets that can
modify their own firing rules at runtime. However, most of the basic decidable prop-
erties of Petri nets such as reachability, place boundedness are lost for this extended
model. In[6], the authors developed a Reconfigurable Petri Nets (RPN) for modeling
adaptable multimedia and protocols that can self-modify during execution, where the
reconfiguration behaviour in Petri nets are modeled by novel modifier places. The work
in [7] presented net rewriting systems that are an extension of Petri nets. The concept of
rewriting rules was depicted, where the execution of a rewriting can change the config-
uration of a Petri net. Reconfigurable timed net condition/event systems (R-TNCESs)
are first developed in [4]. The authors aim to optimal model reconfigurable discrete
event control systems (RDECS). An R-TNCES is modular and the reconfigurable con-
trol ideas are applied in the formalism directly [8]. All these methods are efficient in
their concerned fields. However, most of the proposed formal models lack of modular-
ity, cannot allow the compact and concise modeling of self-reconfigurability of complex
systems. Most importantly, none of them is qualified in modeling DRCSs.
We mention the works of [3] and [9], where the authors defined a multi-agent archi-
tecture for distributed reconfigurable embedded systems. For each device, a reconfigu-
ration agent modeled by a nested state machine is associated in order to handle its local
reconfiguration scenarios. Furthermore, for the purpose of coherent reconfigurations of
distributed devices, an inter-agents communication protocol was developed, which is
based on well-defined coordination matrices held by a coordination agent. Neverthe-
less, the proposed protocol is limited to treat only one reconfiguration requirement in
the case of multiple requirements arising simultaneously. Therefore, in this work, we
propose a novel multi-agent architecture and a new communication protocol in order
to handle all possible reconfiguration scenarios in a DRCS including treating multiple
concurrent requirements.
By using the novel multi-agent architecture, each reconfigurable device is assigned
with a special agent named reconfiguration sub-controller agent to manage its local
automatic reconfigurations. With the new communication protocol that regulates the
interaction among agents, the consistency of agents is solved without any mechanism
such as a special coordinator. Besides, each reconfiguration sub-controller agent han-
dles a set of Decision Matrices for treating with concurrent reconfiguration require-
ments from different agents. The concept of Decision Matrix was inspired from the
concept of Coordination Matrix defined in [9].
In this paper, the RECATNet [10] is applied to model each reconfiguration sub-
controller agent, which is a high-level algebraic net dedicated to the modeling and the
analysis of interactions in collaborative and distributed systems with dynamic structure.
In addition, the distributed reconfiguration processes are modeled by ECATNet [10].
To check the rationality and correctness of the proposed approach, the model checker
Maude [11] is applied to check the linear temporal logic (LTL) based properties. More-
over, the proposed approach is illustrated by a virtual distributed reconfigurable produc-
tion system that is composed of two physically reconfigurable benchmark production
devices: FESTO and EnAS. Their prototypes are available at Martin Luther University
[3],[4]http://aut.informatik.uni-halle.de/.
The remainder of this paper is organized as follows. Section 2 recalls the basic con-
cepts of Recursive ECATNet. The virtual reconfigurable distributed control system that
we use as running example is introduced in Section 3 before the explanation of the pro-
posed approach in Section 4 including the RECATNet and ECATNet based modeling.
After that, the verification of the obtained models using the model checker Maude is de-
scribed in Section 5. Finally, section 6 concludes this paper and depicts further research
plans of the authors.
2 Recursive ECATNet Review
Recursive ECATNets (abbreviated RECATNets) are a kind of high level algebraic Petri
nets combining the expressive power of abstract data types and Recursive Petri nets
[12]. Each place in such a net is associated to a sort (i.e. a data type of the underlying
algebraic specification associated to this net). The marking of a place is a multiset of
algebraic terms (without variables) of the same sort of this place. Moreover, transitions
in RECATNet are partitioned into two types : elementary (Fig.1) and abstract transi-
tions (Fig.1(b)). Each abstract transition is associated to a starting marking represented
graphically in a frame. A capacity associated to a place p specifies the number of alge-
braic terms which can be contained in this place for each element of the sort associated
to p. As shown in Fig.1, the places p and p0 are respectively associated to the sorts s
p:s(c) telt p':s'(c') p:s(c) tabs[CT(p'',tabs)] p':s'(c')
IC(p, telt) IC(p, tabs)
DT(p, telt) CT(p', telt) DT(p, tabs) CT(p', tabs)
TC(telt) TC(tabs)
(a) Elementary transition (b) Abstract transition
Fig. 1. Transition types in RECATNets
and s0 and to the capacity c and c0 . An arc from an input place p to a transition t (ele-
mentary or abstract) is labelled by two algebraic expressions IC(p, t) (Input Condition)
and DT (p, t) (Destroyed Tokens). The expression IC(p, t) specifies the partial condi-
tion on the marking of the place p for the enabling of t (see Table.1). The expression
DT (p, t) specifies the multiset of terms to be removed from the marking of place p
when t is fired. Also, each transition t may be labelled by a Boolean expression T C(t)
which specifies an additional enabling condition on the values taken by contextual vari-
ables of t (i.e. local variables of the expressions IC and DT labelling all the input arcs
of t). When the condition T C(t) is omitted, the default value is the term T rue. For
an elementary transition t, an output arc (t, p0 ) connecting this transition t to a place
p0 is labelled by the expression CT (t, p0 ) (Created Tokens). However, for an abstract
transition t, an output arc (t, p0 ) is labelled by the expression < i > CT (t, p0 ) (In-
dexed Created Tokens). These two algebraic expressions specify the multiset of terms
to produce in the output place p0 when the transition t is fired. In the graphical repre-
sentation of RECATNets, we note the capacity of a place regarding an element of its
sort only if this number is finite. If IC(p, t) =def DT (p, t) on input arc (p, t) (e.g.
IC(p, t) = a+ and DT (p, t) = a), the expression DT (p, t) is omitted on this arc.
In what follows, we note Spec = (S, E) an algebraic specification of an abstract data
type associated to a RECATNet, whereΣ = (S, OP ) is its multi-sort signatureT (S is
a finite set of sort symbols and OP is a finite set operations, such OP S = φ). E
T to Spec. X = (Xs )s∈S is a set of disjoint variables
is the set of equations associated
associated to Spec where OP X = φ and Xs is the set of variables of sort s. We
denote by TΣ,s (X) the set of S-sorted S-terms with variables in the set X.[TΣ (X)]⊕
denotes the set of the multisets of the Σ-terms TΣ (X) where the multiset union op-
erator (⊕) is associative, commutative and admits the empty multiset φ as the identity
element. For a transition t, X(t) denotes the set of the variables of the context of this
transition and Assign(t) denotes the set of all the possible affectations of this variables
set, i.e.Assign(t) = {sub : X(t) → TΣ (φ) | xi ∈ X(t) of sort s, sub(xi ) ∈ TΣ,s (φ)}
Definition 1. (Recursive ECATNets). A recursive ECATNet is a tuple RECAT N et =
(Spec, P, T, sort, Cap, IC, DT, CT, T C, I, Υ, ICT ) where:
– Spec = (Σ, E) is a many sorted algebra where the sorts domains are finite (with
Σ = (S, OP ) ), and X = (Xs )s∈S is a set of S-sorted variables
– P is a finite set of places.
S T
– T = Telt Tabs is finite set of transitions (T P = φ) partitioned into abstract
and elementary ones. Tabs and Telt denoted the set of abstract and elementary
transitions.
– sort: P → S, is a mapping called a sort assignment.
S
– Cap: is a P-vector on capacity places: p∈P, Cap(p): TΣ (φ) → N {∞},
– IC : PS× T →S[TΣ (X)]∗⊕ where [TΣ (X)]∗⊕ =
{α+ } {α− } {α0 }, such that α ∈ [TΣ,sort(p) (X)]⊕
– DT : P × T → [TΣ (X)]⊕ , such that DT (p, t) ∈ [TΣ,sort(p) (X)]⊕ ,
– CT : P × T → [TΣ (X)]⊕ , such that DT (p, t) ∈ [TΣ,sort(p) (X)]⊕ ,
– T C : T → [TΣ,bool (X)],
– I is a finite set of indices, called termination indices,
– Υ is a family, indexed by I, of effective representation of semi-linear sets of final
markings,
– ICT : P × Tabs × I → [TΣ (X)]⊕ , where ICT (p, t, i) ∈ [TΣ,sort(p) (X)]⊕ .
Table 1. Different forms of Input Condition IC(p,t)
IC(p,t) Enabling Condition
a0 The marking of the place p must be equal to a (e.g. IC(p, t) = φ0
means the marking of p must empty)
a+ The marking of the place p must include a (e.g. IC(p, t) = φ+ means
condition is always satisfied)
a− The marking of the place p must not include a, with a 6= φ
α1 ∧ α2 Conditions α1 and α2 are both true
α1 ∨ α2 α1 or α2 is true
Informally, a RECATNet generates during its execution a dynamical tree of marked
threads called an extended marking, which reflects the global state of such net. This
latter denotes the fatherhood relation between the generated threads (describing the
inter-threads calls). Each of these threads has its own execution context.
Definition 2. (Extended marking). An extended marking of a RECATNet is a labelled
rooted tree denoted T r = hV, M, E, Ai where:
– V is the set of nodes (i.e. threads),
– M is a Mapping V → [TΣ (φ)]⊕ associating an ordinary marking with each node
of the tree, such that ∀v ∈ V, ∀p ∈ P, M (v)(p) ≤ Cap(p),
– E ⊆ V × V is the set of edges,
– A is a mapping E → Tabs associating an abstract transition with each edge.
Example 1. Fig2(a) illustrates the characteristic features of RECATNet. (1) An abstract
transition t is followed by the starting marking CT (p, t). For instance SendRequest
is an abstract transition and CT (SendRq) = (Request, Rq) where Rq represnets, for
instance, the request of client product. The firing of SendRequest will create a thread
that starts with one token Rq in place Request. (2) Any termination set can be defined
concisely based on place marking. for instance, Υ0 specifies the final marking of threads
such that the place EndRequest contains at least one token. (3) The index of termina-
tion (< 0 > or < 1 >) specifies the place ResultOK or ResultN otOK, respectively,
will be marked after the termination of the created thread.
Note that contrary to ordinary nets, RECATNet are often disconnected since each con-
nected component may be activated by the firing of abstract transitions.
EnsRequest Request v0 v0
v0,SendRq
Rq+ Rq
SendRq() SendRq
ReceivReq
v0 v1
<0>Rq <1>Rq
RqReceived v0,SendRq
SendRq SendRq
Rq+ Rq+
RequestOk RequestNotOk v1 v2 v0
ResultOk ResultNotOk
Ok NotOk SendRq SendRq
v1,ReceivReq
Υ 0={M ∣M ( EndRequest =Ok)}
EndRequest v1 v2
Υ 1={M∣M ( EndRequest =NotOk )}
(a) RECATNet (b) Firing sequence
Fig. 2. Example of a RECATNet and one possible firing sequence
Example 2. Fig2(b) highlights a possible firing sequence of the RECATNet represented
in Fig2(a). The graphical representation of any extended marking T r is a tree where
an arc v1 (m1 ) → v2 (m2 ) labeled by tabs means that v2 is a child of v1 created by
firing abstract transition tabs and m1 (resp. m2 ) is the marking of v1 (resp. v2 ). Note
that the initial extende marking is T r0 is reduced to a single node v0 whose marking
is < EnsRequest, (Rq1; Rq2; Rq3) >. More details about RECATNets such as firing
transitions and generating extended reachability graph are presented in [10][13]. The
usefulness of the formalism of RECATNet is: (1) modeling and analysis of interactions
in distributed systems having a dynamic structure and (2) its semantic may be defined
in terms of conditional rewriting logic [14] therefore, the model-checker MAUDE [11]
can be used to check its behavioural properties. This paper applies RECATNet to model
the sub-controllers in the proposed multi-controller based multi-agent architecture.
3 Reconfiguration of Automated Production Systems
In this research work, we use a virtual distributed system composed of two physically
reconfigurable production devices: FESTO and EnAS as a running example. We as-
sume that the two devices cooperate to manufacture workpieces and some particular
reconfiguration scenarios can be applied to them according to well-defined conditions.
3.1 FESTO
It is composed of three units: distribution, test and processing units. The distribution unit
is composed of a pneumatic feeder and a converter to forward cylindrical work pieces
from a stack to the testing unit which is composed of the detector, the tester and the
elevator. The testing unit performs checks of work pieces for height, material type and
color. Work pieces that successfully pass this check are forwarded to the rotating disk
of the processing unit where the drilling of the work piece is performed. We assume in
this work two drilling machines Dr1 and Dr2 to drill pieces. The result of the drilling
operation is next checked by a checking machine and the work piece is forwarded to
another mechanical unit. Four production modes (called local reconfigurations) can be
performed by FESTO.
– Light1: For this production mode, only the drilling machine Dr1 is used;
– Light2 : To drill work pieces for this production mode, only the drilling machineDr2
is used;
– M edium: Medium production mode, where Dr1 and Dr2 are used alternatively;
– High: For this production mode, where Dr1 and Dr2 are used at the same time in
order to accelerate the production.
Ligth1 is the default production mode of FESTO and the system completely stops in
the worst case if the two drilling machines are broken. We assume that only light and
medium production modes are interchangeable, so are medium and high production
modes. The high production mode can be transformed into light production mode di-
rectly, but the reverse is not allowed.
3.2 EnAS
It transports work pieces from FESTO into storage units. The work pieces shall be
placed inside tins to close with caps afterwards. The EnAS is mainly composed of
a belt, two jack stations (J1 and J2) and two gripper stations (G1 and G2). The jack
stations place new drilled work pieces from FESTO and close tins with caps, whereas
the gripper stations remove charged tins from the belt into storage units. Initially, the
belt moves a particular pallet containing a tin and a cap into the first jack station J1.
Three production modes can be performed by EnAS.
– P olicy1: The jack station J1 places a new work piece from FESTO in a tin before
closing the tin with the cap. In this case, the gripper station G1 removes the tin from
the belt into a storage station;
– P olicy2: When the jack station J1 is broken, an empty tin is displaced to the jack
station J2, where a work piece and a cup are put. The closed tin is displaced there-
after on the belt to the gripper station G2 for an evacuation to a storage station;
– P olicy3: The jack station J1 places just a drilled work piece in the tin that is moved
thereafter into the jack station J2 to place a second new work piece. Once J2 closes
the tin with a cap, the belt moves the pallet into the gripper station G2 to remove
the tin (with two work pieces) into a storage station.
P olicy1 is the default behaviour mode of EnAS and the system completely stops in
the worst case if the two jack stations are broken. We assume that only P olicy1 and
P olicy3 are interchangeable. We suppose that the two benchmark production systems
FESTO and EnAS are logically linked to coordinate their tasks. The allowed compo-
sitions of behaviour modes of the two systems are defined in Tab.2. In fact, when a
Table 2. Possible behaviour compositions of FESTO and EnAS
(FESTO, EnAS) (FESTO, EnAS)
(Light1, Policy1) (Medium, Policy1)
(Light1, Policy2) (Medium, Policy2)
(Light2, Policy1) (Medium, Policy3)
(Light2, Policy2) (High, Policy3)
local reconfiguration is planned to be applied to one of these two devices, the other one
should have a proper reaction as a response to the planned reconfiguration in order to
guarantee the coherence of the whole system.
4 Modelling Distributed Reconfigurable Control System
4.1 Multi-Agent Architecture For Distributed Reconfigurable Control Systems
We define a multi-agent architecture for distributed reconfigurable systems where each
reconfigurable sub-controller agent is assigned to a device in order to control its local
reconfiguration. In fact, any reconfiguration scenario cannot be applied within a de-
vice until its sub-controller receives an acceptance command from the others. The sub-
controller may coordinate through a communication network, since any uncontrolled
automatic reconfiguration applied to a device may cause serious disturbance on others.
Fig.3 shows our proposed architecture. Assume that the architecture manages n net-
worked reconfigurable devices. A multi-agent architecture Π is defined by: Π = (Λ, ρ)
Where Λ = (Λ1 , ..., Λn ) is a set of n sub-controllers agents and ρ represents the com-
munication protocol that defines the interaction rules between the set of sub-controllers
agents.
Device
Device
Sub-Controller Sub-Controller
Agent Agent
Communication
Protocol
Device
Device
Sub-Controller Sub-Controller
Agent Agent
Fig. 3. Architecture of Distributed Control Systems
4.2 Communication Protocol
In this section, we show the main function of communication protocol ρ used in order
to coordinate between the sub-controller agents.
When a particular sub-controller agent Λi would to reconfigure itself from the cthi con-
figuration into the gith configuration, it sends, broadcasts, the following request to the
other sub-controller agents:
request(Λi , Λj , gi ). where j = 1, n and j 6= i
For each request received by the sub-controller agent Λj , it selects the Decision Matrix
that will be applied. Let DMj be such a matrix. It is m × 2 integer, where m is the
number of possible local configurations of Λj while the sub-controller agent Λi is in the
gith configuration. A row vector, denoted by rowj , of DMj corresponds to a particular
configuration of Λi and Λj . For the determinacy of the local configuration of Λj , only
one of the row vector in DMj is finally chosen. We assume, in this current research,
that all row vectors of DMj have the same priority.
Example 3 (Decision Matrix). We show bellow a decision matrix built when receives
possible reconfiguration requirements from Λ1 .
L1 P 1
DM2,L1 =
L1 P 2
The matrix DM2,L1 is applied when sub-controller agent Λ1 requires to transform
FESTO into Light1. In fact, if Light1 is activated in Λ1 , then P olicy1 or P olicy2
of Λ2 can be activated.
Let denote by rowkj = rowk1 j j
, rowk2 , where rowk1j
= gi , the k th row vector to
be applied by the sub-controller Λj . Let denote the current behaviour of each sub-
controller agent Λj by cj . The possible results of sub-controller agent Λj are as follows:
– If no row can be selected in DMj , then Λj sends the following message to the
sub-controller agent Λi : reject(Λj , Λi , cj ). It means that the sub-controller agent
Λj reject the reconfiguration requirement of Λi .
– Else
j
• If rk2 = cj , then the sub-controller agent Λj sends the following message to the
sub-controller agent Λi : accept(Λj , Λi , cj ). It means that the sub-controller Λj
agent accept the reconfiguration requirement sent by Λi without need to change
its local behaviour.
j
• If rk2 6= cj , and suppose that there exist some rows (suppose the number is
w) in the matrix holt by Λj in which rkj l 2 6= cj where l = 1, w, then the sub-
controller agent Λj sends the following message to the sub-controller agent
Λi : possible reconf igure(Λj , Λi , rkj 1 2 , rkj 2 2 , ..., rkj w 2 ). It means that the sub-
controller agent Λj accepts the reconfiguration requirement sent by Λi , and
needs to apply one of the set of possible reconfigurations requirement rkj l 2 .
Let denote by βapply the set of sub-controller agents need to apply a local
reconfiguration during a distributed reconfiguration process.
When the sub-controller Λi receives a response from all the other sub-controller agents:
– If there is one reject message received, then it sends to the sub-controller agents of
j
the set βapply the following message: ref use(Λi , Λj , rk2 );
– Else, a set of new distributed configurations is formed by combining all the received
possible reconfigurations from sub-controllers Λj , let denote it by DΠ .
1 n
• If there is a such distributed reconfiguration d = (rk2 , ..., gi , ..., rk2 ) ∈ DΠ
that can be deduced from its Decision Matrices then, Λi sends to the sub-
j
controller agents of the set βapply the following message : apply(Λi , Λj , rk2 );
j
• Else, Λi sends ref use(Λi , Λj , rk2 ).
Example 4. We show in Fig.5 required interactions between sub-controller agents when
FESTO would to apply Ligth2 production policy when drilling machine Dr1 breaks
down. The row vector (L2, P 2) is finally selected by the sub-controller agent of EnAS
i.e. row2 = (L2, P 2). From the selected row, EnAS needs to change its local be-
havior, so it sends a message possible reconf igure(Λ2 , Λ1 , P 2) to FESTO. There-
fore, there is no reject message received in FESTO, so FESTO sends to EnAS message
apply(Λ1 , Λ2 , P 2) in order to apply its new local reconfiguration.
We model each possible distributed reconfiguration process by ECATNet composed of
(βapply + 1) traces where each trace is composed of places and transitions corresponds
to coordination result of a sub-controller agents. Each trace starts with a place p, ends
with a place p0 , and two transitions between the two places. We distinguish two types
of traces:
– A trace which corresponds to the result of a sub-controller that sends a reconfigu-
ration requirement. In this case, a trace is denoted by p, taccept /treject , p0 , where
taccept and treject are in conflict. The firing of taccept means that the required re-
configuration is accepted, whereas firing of treject means that the reconfiguration
requirement is rejected at least by one sub-controller agent.
– A trace which corresponds to the result of a sub-controller that does not send a
reconfiguration requirement. In this case, a trace is denoted by p, tapply /tref use , p0 ,
where tapply and tref use are in conflict. The firing of tapply means that the sub-
controller agent receives an order to apply the required reconfiguration, whereas
(
DM 2, L2 =
L2
L2
P1
P2 )
FESTO agent EnAS agent
c1 = L1 c2 = P1
needs reconfiguration : L2
request (Λ 1, Λ 2, L2)
possible −reconfigure ( Λ 2, Λ 1, P2)
apply (Λ 1, Λ 2, P2)
local reconfiguration local reconfiguration
from L1 to L2 from P1 to P2
Fig. 4. Coordination between FESTO and EnAS when drilling machine Dr1 is broken
the firing of tref use means that the sub-controller agent receives an order to not
apply the required reconfiguration.
Example 5. Fig.5 shows the ECATNet based model of the distributed reconfiguration
process in Example 4. The model of the selected vector (L2, P 2) has two traces: the first
p0 , taccept /treject , rep1 corresponds to the result of the reconfiguration requirements
of FESTO and the second p1 , tapply /tref use , rep2 corresponds to the result of the re-
configuration requirements of EnAS according to the reconfiguration requirements of
FESTO. For the first trace, according to selected row vector, the sub-controller agent
of EnAS Accepts the reconfiguration requirement of FESTO. In this case, the transi-
tion taccept will be enabled because its associated condition (b1 = b2) is true. For the
second trace, EnAS needs to apply the new selected reconfiguration. In this case, the
transition tapply will be enabled i.e. its associated condition (g1 = g2) is true.
dreconf1 : FData sp2 : DConf dreconf2 : EData Spec DCONFPROCESS
(L2, P2)
sorts Data FData EData DConf List .
ops accept, reject, apply, refuse: Data .
b2 g2 ops L1 L2 Me Hi : FData .
(b1,g1) (b1,g1)
t0 t1 ops P1 P2 P3 : EData .
(b1,b2) (g1,g2) ops _,_ : FData EData : DConf.
ops _,_ : FData FData : List .
p0 : List p1 : List ops _,_ : EData EData : List .
(b1,b2) (g1,g2) vars g1 g2 : EData .
(b1,b2) (g1,g2)
taccept treject tapply trefuse vars b1 b2 : FData .
b1=b2 b1≠b2 g1=g2 g1≠g2 End.
accept reject apply refuse Υ 11={M∣M ( rep1 =accept)}
Υ 12={M∣M ( rep1 =reject )}
rep1 : Data rep2 : Data
Υ 21={M ∣M (rep 2=apply)}
Υ 22={M ∣M (rep 2=refuse)}
Fig. 5. ECATNet model of a distributed reconfiguration process
4.3 Sub-Controller Agent
The main aim of a sub-controller agent is controlling the local reconfigurations of as-
sociated device. This agent should be self-reconfigurable. In fact, the agent may offer
multiple behaviours and dynamic transformations of them according to changed en-
vironment while keeps the correctness and safety. In fact, and in order to specify the
dynamic structure of each sub-controller agent Λi , i = 1, n we use a marked RECAT-
Net, i.e. Λi = (RNi , M0i ) where RNi = (Speci , ..., ICTi ) is a Recursive ECATNet
that represents the dynamic structure of this agent and M0i is the initial marking which
represents its initial local behaviour.
Example 6 (FESTO). We present in FIG.6(a). the RECATNet of our sub-controller
agent Λ1 of FESTO. As described above, the sub-controller agent can perform four
inevent : Event p: Token inevent : Event p:Token
token
token
t+ Spec EnAS
sp0 : FData tgenLB
g token g tgenLB token sorts EData Event .
Spec FESTO sp0 : EData
sorts Token FData Event . ops P1 P2 P3 : EData .
g+ t0 sp2 : FData ops L1 L2 Me Hi : FData . t0 sp2 : EData ops jacks1-Down : Event .
sp1 : FData sp1 : EData g+ vars c g : EData .
g ops dr1-Down : Event . g
L1 <12>token vars c g : FData . P1 <22>token End.
c c
c≠g g var t : Token . c≠g g
End.
c t1 c t1
Condition
g <11>g <12>g g <21>g <22>g Condition
((c=L1)˄(g=L2)) ˅((c=L1)˄(g=Me)) ˅
t2 ((c=Me)˄(g=L1)) ˅((c=Me)˄(g=L2)) ˅ t2 ((c=P1)˄(g=P2)) ˅((c=P1)˄(g=P3)) ˅
g g ((c=P3)˄(g=P1)) ˅((c=P3)˄(g=P2))
((c=Me)˄(g=Hi)) ˅((c=Hi)˄(g=L1)) ˅
((c=Hi)˄(g=L2)) ˅((c=Hi)˄(g=Me))
Condition sp4 : FData sp3 : FData Condition sp4 : EData sp3 : EData
(a) FESTO Λ1 (b) EnAS Λ2
Fig. 6. RECATNets model of the sub-controller agents
policies Ligth1, Ligth2, M edium and High. They can be modelled as terms, accord-
ing to our algebraic specification, by L1, L2, M e and Hi. The initial marking of this
agent is M01 =< sp1 , L1 > that represents the initial local behaviour Ligth1. As
shown in Fig.7, the specification includes on input place (event). By means of the in-
put place, events are received from FESTO (i.e drill machine Dr1 is break down,...) or
user requirements. For each new received event, the sub-controller agent generates its
associate local state in place sp0 . For instance, when drill machine Dr1 is break down,
the place event will receive a token dr1−Down and transition tgenLB can be fired and
generate the lacal bahaviour L2 where the sub-controller needs to transform. Marking
of place p allows to treate one by one received events. In order to apply the new gener-
ated local behaviour, the sub-controller will fire the set of transitions t0, t1 and t2 which
defines the self-reconfiguration of the sub-controller agent. The enabling of transition
t0 allows to generate the requirement behaviour g that must be different of the current
behaviour c where c, g ∈ {L1, L2, M e, Hi} . The abstract transition t1 allows to check
if the sub-controller can be applied the new requirement. When the sub-controller re-
ceiving a response, two cases can be distinguished: The first one represented by the
termination index < 12 > means that the new requirement of the sub-controller is
rejected. The second one represented by the termination index < 11 > means that
the new requirement is accepted and the sub-controller can apply the new requirement
by enabling the transition t2. This last transition represents the local reconfiguration
transformation. We associate to this transition an additional enabling condition which
corresponds to eight possible local reconfiguration scenarios can be applied to FESTO.
For instance, condition (c = L1 ∧ g = L2) means that the sub-controller agent may be
transformed from local behaviour L1 to L2.
Example 7 (EnAS). The RECATNet model of the sub-controller agent Λ2 for EnAS, as
shown in Fig.8, is similar to that of the sub-controller agent Λ1 for FESTO, except that
Λ2 can perform three policies P olicy1, P olicy2 and P olicy3 modelled by a closed
terms P 1, P 2 and P 3. The initial marking of this agent is M02 =< sp1 , P 1 > that
represents the initial local behaviour P olicy1. Four different reconfiguration scenarios
can be applied to EnAS represented by conditions associated to transition t2. The spec-
ification of EnAS includes one input place (event). It means that the sub-controller can
receive in this place events produced by the jack station J1 or J2 or user requirements.
5 Verification of DRCS
For analysing the obtained RECATNet, we have expressed its semantic into rewriting
logic [14], the input of the model-checker Maude. The checked properties have to be
expressed using Linear Temporal Logic (LTL).
5.1 RECATNet semantics in terms of rewriting logic
Since we choose to express the RECATNet semantics in terms of rewriting logic, we de-
fine each RECATNet as a conditional theory like in [13], where transitions firing and cut
step execution are formally expressed by labelled rewrites rules. Each extended mark-
ing T r is expressed, in a recursive way, as a term [M T h, tabs, T hreadChilds], where
M T h represents the internal marking of T h, tabs represents the name of the abstract
transition whose firing (in its thread father) gave birth to the thread T h. Note that the
root thread is not generated by any abstract transition, so the abstract transition which
gave birth to it is represented by the constant nullT rans. The term T hreadChilds rep-
resents a finite multiset of threads generated by the firing of abstract transitions in the
thread T h. We denote by the constant nullT hread, the empty thread. Consequently, the
extended marking T r represented in Fig.7 is expressed as a general term of sort T hread
with the following recursive form: [M T h0 , nullT rans, [M T h1 , tabs1 , [M T h11 , tabs11
, ...]...[M T h1n , tabs1n , ...]]...[M T hn , tabsn , [M T hn1 , tabsn1 , ...]...[M T hnn , tabsnn , ...]]]
where M T h0 is the marking of the root thread.
Mth0
tabs1 tabsn
Mth1 …................ Mthn
tabs11 tabs1n tabsn1 tabsnn
Mth11 …........... Mth1n Mthn1 …........... Mthnn
Fig. 7. General form of an extended marking
The structure of distributed states of RECATNets is formalized by the following equa-
tional theories.
fmod THREAD is
pr MARKING .
sorts Thread Trans TransAbs .
subsort TransAbs < Trans .
op nullTrans : -> TransAbs .
op nullThread : -> Thread .
op [_,_,_]:Marking TransAbs Thread ->Thread .
op _ _ :Thread Thread ->Thread [assoc comm id: nullThread] .
endfm
Where module M arking is a set of P lace − M arking defined in rewriting logic as
follows:
fmod MARKING is
pr PLACE-MARKING .
sort Marking .
subsort Place-marking < Marking .
op em : -> Marking . --- empty marking
op _(*)_ : Marking Marking -> Marking [assoc comm id: em] .
endfm
fmod PLACE-MARKING is
sorts Place Multiset Place-marking .
op ems : -> Multiset . --- empty Multiset
op _(+)_ : Multiset Multiset -> Multiset [assoc comm id: ems] .
op <_;_> : Place Multiset -> Place-marking .
endfm
Each firing step in a RECATNet is expressed by a rewrite rule of the form M =>
M 0 if Cond which means that a fragment of the RECATNet state fitting pattern M can
change to a new local state fitting pattern M 0 if the condition Cond holds. We give the
general form of the rewrite rules describing the behaviour of RECATNets firing steps:
– Rule associated to an elementary transition
crl[telt]: (*) =>
(*) if (InputCond and TC(telt)
and Nbr(mp’(+)CT(p’,telt) < Cap(p’))) .
– Rule associated to an abstract transition
crl[tabs]:[M (*) , T, Th] =>
[M (*) , T, Th [, tabs, nullThread]]
if (InputCond and TC(tabs)) .
– Rule associated to a cut step
crl[cut]: , T, mThf [M (*) ,
tabs, mTh]> =>[Mf (*) ]
if ( Υ i and Nbr(mp’(+) ICT(p’,tabs,i) < Cap(p’)) .
For instance, if we consider the RECATNet of Fig.6(a), the rewrite rule describing the
elementary transition labelled t0 is given as follows:
crl[t0]:(*) => (*) if c =/= g .
Another example, the rewrite rule describing the abstract transition labelled t1 is given
as follows:
rl[t1]:[,T,Th] => [M,T,Th [,t1,nullThread]] .
After defining the semantics of RECATNet in terms of rewriting rules, the model-
checker Maude can be used.
5.2 Implementation using the Maude Tool
In this section, we plan to check the correct response of the whole system to the recon-
figuration request and the valid behavior of sub-controller agents after the application
of a distributed reconfiguration scenario.
Example 8. Let take the example shown in Fig.4. The initial distributed configuration is
d = (L1, P 1), where L1 represnts the local behavior Ligth1 of FESTO and P 1 repre-
sents the local behavior P olicy1 of EnAS. This distributed configuration is specified in
rewriting logic as follows:
eq initDistState = < sp11 ; L1 >(*)< sp12 ; P1 > .
From Fig.4, when drill machine Dr1 is broken, the sub-controller agent of FESTO
needs to change its local behaviour to L2. The new selected distributed configuration
from Decision Matrices is d = (L2, P 2).The following equation, in term of rewriting
logic, specifies the new distribute state of the whole system to be reached.
eq < sp11 ; L2 >(*)< sp12 ; P2 > |= newDistState = true .
In order to check the valid behavior of sub-controller agents, we call the model-checker
of Maude as follows:
Model-Check(initDistState, <> newDistState).
This means that starting from an initial distribute state, every possible execution path
reaches the new distributed state. The symbol <> denotes the temporal operator Eventually.
In Fig.8, verification shows that the specified formula is true.
Fig. 8. Model Checking under Maude
Example9. Let take another example and we focus on the case, if a response command is
received, whether the sub-controller FESTO can respond and select a proper behaviour.
First, we define predicates:
Example9. Let take another example and we focus on the case, if a response command is
received, whether the sub-controller FESTO can respond and select a proper behavior. First,
we define predicates:
op Medium-Mode Ligth1-Mode : -> Prop .
op Medium-Mode Ligth1-Mode : -> Prop .
ops Drill-Down Reply
ops Drill-Down : Multiset
Reply : Multiset ->
-> Prop
Prop ..
eq (*) M |= Medium-Mode = true .
eq < sp11 ; Me > (*) M |= Medium-Mode = true .
eq < sp11 ; L1>(*) M |= Ligth1-Mode = true .
eq (
eq < sp11 ; L1*)> M
(*)|=M Reply(accept)=true
|= Ligth1-Mode = true ..
eq (*) M |= Drill-Down(dr2-down)=true .
eq < rep1 ; accept > (*) M |= Reply(accept) = true .
Now, let’s
eq consider the following
< in1-event LTL> property:
; dr2-down (*) M |= Drill-Down(dr2-down) =
true .
[] ( Medium-Mode /\ Drill-Down(dr2-down) /\ Reply(accept)
Now,
=> let’s
<> consider the following).
Ligth1-Mode LTL property:
[] ( Medium-Mode /\ Drill-Down(dr2-down) /\ Reply(accept) =>
This LTL formula means that, always, if FESTO is in M edium behaviour, drill ma-
<> Ligth1-Mode ).
chine Dr2 is broken and command accept is received, FESTO will eventually select
the Ligth1
This LTL formula means
behaviour. that, always,
Finally, we callif FESTO
Maude is in Medium
LTL behavior,
model checkerdrill machine
to checkDr2this
is prop-
broken and
erty (see Fig.9). command accept is received, FESTO will eventually select the Ligth1 behavior.
Finally, we call Maude LTL model checker to check this property (see Figure X.).
Fig. 9. Model checking of the property
6 Conclusion and Future Works
This research work copes with the reconfiguration and coordination issues of DRCSs. A
novel multi-agent architecture is proposed such that a device has a particular reconfig-
urable sub-controller agent to especially manage its local reconfiguration. The problem
of concurrent reconfiguration requirements are solved by proposing a new communi-
cation protocol where Decision Matrices are applied by the sub-controller agents. The
proposed approach is modeled by the formalism of RECATNets and checked by using
the MAUDE model-checker. A virtual reconfigurable distributed production system is
applied as a running example to illustrate the whole work.
In the future, we will plan to extend our work in order to model and anlyse time-
constrained DRCSs. In this case, we will use an extended version of our formalism
called time-RECATNets (T-RECATNets)[13]. Therefore, one can verify some proper-
ties with respect to time constraints using Real-Time MAUDE model-checker[15].
References
1. Y. Koren, U. Heisel, F. Jovane, T. Moriwaki, G. UIsoy, and H. V. Brussel, “Reconfigurable
manufacturing systems,” CIRP Annals- Manufacturing Technology, vol. 48, pp. 527–540,
1999.
2. M. G. Mehrabi, A. G. Ulsoy, and Y. Koren, “Reconfigurable manufacturing systems: key
to future manufacturing,” Journal of Intelligent Manufacturing, vol. 11, no. 4, pp. 403–419,
2000.
3. M. Khalgui and H. Hanisch, “Automatic nces-based specification and sesa-based verification
of feasible control components in benchmark production systems,” International Journal of
Modeling, Identification and Control, vol. 12, no. 3, pp. 223–243, 2011.
4. J. Zhang, M. Khalgui, Z. Li, O. Mosbahi, and A. Al-Ahmari, “R-tnces: A novel formalism
for reconfigurable discrete event control systems,” Systems, Man, and Cybernetics: Systems,
IEEE Transactions on, vol. 43, no. 4, pp. 757–772, 2013.
5. R. Valk, “Self-modifying nets, a natural extension of petri nets,” in Proceedings of the Fifth
Colloquium on Automata, Languages and Programming, 1978, pp. 464–476.
6. S. U. Guan and S.-S. Lim, “Modeling adaptable multimedia and self-modifying protocol
execution.” Future Generation Comp. Syst., vol. 20, no. 1, pp. 123–143, 2004.
7. E. Badouel, M. Llorens, and J. Oliver, “Modeling concurrent systems: Reconfigurable nets,”
in International Conference on Parallel and Distributed Processing Techniques and Appli-
cations, PDPTA. CSREA Press, 2003, pp. 1568–1574.
8. H. M. Hanisch, J. Thieme, A. Luder, and O. Wienhold, “Modeling of plc behavior by means
of timed net condition/event systems,” in Emerging Technologies and Factory Automation
Proceedings, 1997. ETFA ’97., 1997 6th International Conference on, 1997, pp. 391–396.
9. M. Khalgui and O. Mosbahi, “Intelligent distributed control systems,” Inf. Softw. Technol.,
vol. 52, no. 12, pp. 1259–1271, 2010.
10. K. Barkaoui and A. Hicheur, “Towards analysis of flexible and collaborative workflow us-
ing recursive ecatnets,” in Business Process Management Workshops, ser. Lecture Notes in
Computer Science, A. Hofstede, B. Benatallah, and H.-Y. Paik, Eds., 2008, vol. 4928, pp.
232–244.
11. M. Clavel and al., “Maude manual (version 2.3),” 2007. [Online]. Available:
http://maude.cs.uiuc.edu
12. S. Haddad and D. Poitrenaud, “Recursive petri nets: Theory and application to discrete event
systems,” Acta Inf., vol. 44, no. 7, pp. 463–508, Nov. 2007.
13. K. Barkaoui, H. Boucheneb, and A. Hicheur, “Modelling and analysis of time-constrained
flexible workflows with time recursive ecatnets,” ser. Lecture Notes in Computer Science.
Springer Berlin Heidelberg, 2009, vol. 5387, pp. 19–36.
14. R. Bruni and J. Meseguer, “Semantic foundations for generalized rewrite theories,” Theor.
Comput. Sci., vol. 360, no. 1, pp. 386–414, Aug. 2006.
15. P.C. Ölveczky, and J. Meseguer, “ Real-Time Maude: A tool for simulating and analyzing
real-time and hybrid systems“. In 3rd International Workshop on Rewriting Logic and its
Applications (WRLA’00), volume 36 of Electronic Notes in Theoretical Computer Science.
2000.