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.