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 distributed control system has a special self-governed agent named reconfiguration sub-controller agent to manage its local reconfiguration. Accordingly, a communication protocol is developed to handle interaction style among these agents for the purpose of consistency. The proposed architecture is modeled by RECATNets and the distributed reconfiguration process is modeled by an ECATNet. Furthermore, in order to check the correctness of the proposed approach, the model checker Maude is applied, where required properties are specified by Linear Temporal Logic. Finally, a virtual distributed control system contains two reconfigurable devices is applied to illustrate this work.
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 reconfigurations that are implemented by the dynamic addition/removal of software/hardware components, the modification of logic relationship among components, and the adjustment 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 properties 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 configuration 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 control 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 modularity, 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 architecture for distributed reconfigurable embedded systems. For each device, a reconfiguration 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. Nevertheless, 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 handles a set of Decision Matrices for treating with concurrent reconfiguration requirements 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 subcontroller 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. Moreover, the proposed approach is illustrated by a virtual distributed reconfigurable production 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 concepts 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 proposed 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 described in Section 5. Finally, section 6 concludes this paper and depicts further research plans of the authors. 2
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 transitions (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 algebraic 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)
t IC(p, telt) elt p':s'(c') p:s(c) IC(p, tabs)tabs[CT(p'',tabs)] p':s'(c')
(a) Elementary transition
(b) Abstract transition and s0 and to the capacity c and c0. An arc from an input place p to a transition t (elementary 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 condition 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 variables 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) (Indexed 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 representation 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 signature (S is a finite set of sort symbols and OP is a finite set operations, such OP T S = ). E is the set of equations associated to Spec. X = (Xs)s2S is a set of disjoint variables associated to Spec where OP T 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 operator ( ) 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) = fsub : X (t) ! T ( ) j xi 2 X (t) of sort s, sub(xi) 2 T ;s( )g Definition 1. (Recursive ECATNets). A recursive ECATNet is a tuple RECAT N et = (Spec; P; T ; sort; Cap; I C; DT ; CT ; T C; I ; ; I CT ) where: – Spec = ( ; E) is a many sorted algebra where the sorts domains are finite (with = (S; OP ) ), and X = (Xs)s2S is a set of S-sorted variables – P is a finite set of places. – T = Telt S Tabs is finite set of transitions (T 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. – Cap: is a P-vector on capacity places: p2P, Cap(p): T ( ) ! N Sf1g, – I C : P T ! [T (X )] where [T (X )] =
f +g Sf g Sf 0g, such that 2 [T ;sort(p)(X )] – DT : P T ! [T (X )] , such that DT (p; t) 2 [T ;sort(p)(X )] , – CT : P T ! [T (X )] , such that DT (p; t) 2 [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, – I CT : P Tabs
I ! [T (X )] , where I CT (p; t; i) 2 [T ;sort(p)(X )] .
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 8v 2 V; 8p 2 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. (
Note that contrary to ordinary nets, RECATNet are often disconnected since each connected component may be activated by the firing of abstract transitions.
EnsRequest
Rq+ SendRq(<Request,Rq>) <0>Rq <1>Rq
Request Rq
ReceivReq
RqReceived
Rq+ Rq+
RequestOk ResultOk ReΥsu0lt=No{tMOk∣M (EndRequest=Ok)} Ok Υ1={M∣M (EndRequest=NotOk)}
RequestNotOk NotOk
EndRequest (a) RECATNet v0<EnsRequest, (Rq0; Rq1)> v0,SendRq
v0<EnsRequest,ϕ>
SendRq SendRq v1<Request, Rq1> v2<Request, Rq2> v1,ReceivReq v0<EnsRequest, (Rq1)> SendRq v1<Request, Rq1> v0,SendRq
v0<EnsRequest,ϕ>
SendRq SendRq
v1<RqReceived, Rq1> v2<Request, Rq2>
(b) 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: (
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 assume 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
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 directly, but the reverse is not allowed. 3.2
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 thereafter 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 compositions of behaviour modes of the two systems are defined in Tab.2. In fact, when a 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 4.1
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 device until its sub-controller receives an acceptance command from the others. The subcontroller 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 networked reconfigurable devices. A multi-agent architecture is defined by: = ( ; ) Where = ( 1; :::; n) is a set of n sub-controllers agents and represents the communication protocol that defines the interaction rules between the set of sub-controllers agents.
D iecv Sub-ACgoenntrtoller e D ivec Sub-ACgoenntrtoller e
Communication
Protocol
D Sub-Controller ive
Agent ce
D Sub-Controller ive
Agent ec 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 cith configuration 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 gth configuration. A row vector, denoted by rowj , of DMj corresponds to a particular i 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.
DM2;L1 =
L1 P 1 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 = rowkj1; rowkj2 , where rowkj1 = gi, the kth row vector to be applied by the sub-controller j . Let denote the current behaviour of each subcontroller 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.
If rkj2 = 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.
If rkj2 6= cj , and suppose that there exist some rows (suppose the number is w) in the matrix holt by j in which rkjl2 6= cj where l = 1; w, then the subcontroller agent j sends the following message to the sub-controller agent i: possible reconf igure( j ; i; rkj12; rkj22; :::; rkjw2). It means that the subcontroller agent j accepts the reconfiguration requirement sent by i, and needs to apply one of the set of possible reconfigurations requirement rkjl2. 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 the set apply the following message: ref use( i; j ; rkj2); – 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 .
If there is a such distributed reconfiguration d = (rk12; :::; gi; :::; rkn2) 2 D that can be deduced from its Decision Matrices then, i sends to the subcontroller agents of the set apply the following message : apply( i; j ; rkj2); Else, i sends ref use( i; j ; rkj2).
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 behavior, so it sends a message possible reconf igure( 2; 1; P 2) to FESTO. Therefore, 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 reconfiguration 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 reconfiguration 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=trefuse; p0, where tapply and trefuse are in conflict. The firing of tapply means that the subcontroller agent receives an order to apply the required reconfiguration, whereas FESTO agent c1 = L1
EnAS agent
c2 = P1 needs reconfiguration : L2
request (Λ1, Λ2, L2) possible −reconfigure (Λ2, Λ1, P2)
apply (Λ1, Λ2, P2) local reconfiguration from L1 to L2 local reconfiguration from P1 to P2 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 reconfiguration 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 transition 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
(L2, P2) (b1,b2) taccept b1=b2 accept t0 b2
(b1,g1) (b1,g1) (b1,b2) (g1,g2) p0 : List p1 : List (b1t,rbeje2cbt)1≠b2 g1=g(g21,g2) tapply reject apply dreconf2 : EData g2
Spec DCONFPROCESS sorts Data FData EData DConf List . ops accept, reject, apply, refuse: Data .
ops L1 L2 Me Hi : FData . t1 ooppss _P,_1 :PF2DPa3ta:EEDDaatata:. DConf.
ops _,_ : FData FData : List .
ops _,_ : EData EData : List . (g1t,rgefu2sge)1≠g2 vvEaanrrdss. bg11 bg22 :: FEDDaattaa ..
refuse rep1 : Data rep2 : Data Υ11={M∣M ( rep1=accept)} Υ12={M∣M ( rep1=reject )} Υ21={M ∣M (rep2=apply )} Υ22={M ∣M (rep2=refuse)}
Fig. 5. ECATNet model of a distributed reconfiguration process The main aim of a sub-controller agent is controlling the local reconfigurations of associated device. This agent should be self-reconfigurable. In fact, the agent may offer multiple behaviours and dynamic transformations of them according to changed environment 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 RECATNet, 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 policies Ligth1, Ligth2, M edium and High. They can be modelled as terms, according 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 input 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 generated 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 2 fL1; L2; M e; Hig . The abstract transition t1 allows to check if the sub-controller can be applied the new requirement. When the sub-controller receiving 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 specification 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
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
Since we choose to express the RECATNet semantics in terms of rewriting logic, we define 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 marking 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 represents 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.
tabs1
Mth0
tabsn tabs11
Mth1 …................ tabs1n tabsn1
tabsnn
Fig. 7. General form of an extended marking The structure of distributed states of RECATNets is formalized by the following equational 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 Marking is a set of Place Marking 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 => M0 if Cond which means that a fragment of the RECATNet state fitting pattern M can change to a new local state fitting pattern M0 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]:<p, mp (+) DT(p, telt)> (*) <p’, mp’> => <p, mp> (*) <p’, mp’(+)CT(p’,telt)> if (InputCond and TC(telt) and Nbr(mp’(+)CT(p’,telt) < Cap(p’))) . – Rule associated to an abstract transition crl[tabs]:[M (*)<p, mp (+) DT(p, tabs)> , T, Th] => [M (*)<p, mp> , T, Th [<p’’, CT(p’’,tabs) >, tabs, nullThread]] if (InputCond and TC(tabs)) . – Rule associated to a cut step crl[cut]:<Mf (*) <p’, mp’> , T, mThf [M (*) <pfinal, mpfinal>, tabs, mTh]> =>[Mf (*) <p’, mp’ (+) ICT(p’, tabs, i), T, mThf>] 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]:<sp1 ; c>(*)<sp0 ; g> => <sp1;c>(*)<sp2;g> if c =/= g . Another example, the rewrite rule describing the abstract transition labelled t1 is given as follows: rl[t1]:[<sp2 ;g>,T,Th] => [M,T,Th [<ctr1 ;g>,t1,nullThread]] . After defining the semantics of RECATNet in terms of rewriting rules, the modelchecker Maude can be used.
In this section, we plan to check the correct response of the whole system to the reconfiguration 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 represents 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. 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 MedoipumM-edMioudme-MoLdiegtLhi1gt-hM1o-dMeode: :->->PPrroopp .. ops Droiplsl-DrDiolwln-DoRwenplRyepl:y M:ulMutlitsiestet-->> PPrroopp .. eq <sp11 ; Me> (*) M |= Medium-Mode = true . eq < sepq11< s;p1L11>;(M*e) >M(*|)= M L|=igMtehd1i-umM-oMdoede== ttrruuee .. eq <reepq1;<ascpc1e1pt;>L(1*)> M(*)|=M R|=epLliyg(tah1c-cMeopdte)==ttrruuee .. eq <in1-event ; dr2-down> (*) M |= Drill-Down(dr2-down)=true .
eq < rep1 ; accept > (*) M |= Reply(accept) = true .
Now, leet’qs c<onisni1d-eervtehnetfo;llodwr2i-ndgoLwTnL> p(r*o)peMrty|:= Drill-Down(dr2-down) = true . [] ( Medium-Mode =n Drill-Down(dr2-down) =n
N=o>w, l<et>’s cLonisgidterht1he-fMoollodweing)L.TL property: Reply(accept) This LT[L] f(ormMeudliaumm-eMaondse t/h\at,Draliwlla-yDso,wifn(FdErS2-TdOowins)in/\MReedpiluym(acbceehpatv)io=u>r, drill ma<> Ligth1-Mode ). chine Dr2 is broken and command accept is received, FESTO will eventually select the LigtThhi1sLbTLe hfoarvmiuolaurm.eFainnsatlhlayt,, awlweaycsa,lilf FMESaTuOdies iLnTMLedmiumodbeelhacvhioerc,kdreilrl mtoacchhineecDkr2thisis property (seebrFokiegn.9a)n.d 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.).
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 reconfigurable sub-controller agent to especially manage its local reconfiguration. The problem of concurrent reconfiguration requirements are solved by proposing a new communication 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 timeconstrained DRCSs. In this case, we will use an extended version of our formalism called time-RECATNets (T-RECATNets)[13]. Therefore, one can verify some properties with respect to time constraints using Real-Time MAUDE model-checker[15]. 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 Applications, 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 using 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. O¨ 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.