Using High Level Nets for the Design of Recon gurable Manufacturing Systems

Abstract

Recon gurable systems (RSs) are systems were the structure can be changed during the execution of the system. Recon gurable manufacturing systems (RMSs) represent one of the most prominent successes in the RSs technology. Recon guration in RMSs can be motivated by many reasons: a new requirement in the production process, to avoid some problems caused by machines breakdowns, etc. RMSs o er exibility, productivity and e ciency in plants and production lines. Though, the design, realisation and veri cation of RMSs seem to be hard tasks and imply innovative approaches. High level Petri Nets supply the ability to design these systems and to analyse their properties. In this paper, we apply Recon gurable Object Nets (RONs) for the modelling, simulation and analysis of recon gurable manufacturing systems. We present an experience where the recon guration process, in RMSs, is speci ed explicitly as a \Place/transition nets transformation", the simulation is realised using the RON-editor tool, and the analysis exploits the TINAtool (TImed Nets Analyser tool).

-

Manufacturing Systems (MSs) [ 1 ] are widely used in industry. They are characterised by their hybrid aspect and their complexity. A manufacturing system is, usually, composed of a set of components: machines, robots, conveyors, bu ers, and eventually humans. These components co-exist and interact to produce some products. Interactions, between these components, are done explicitly through exchanged messages or implicitly through travelling products during the manufacturing process. The success of a manufacturing system is based on the quality of each component and on the quality of the interactions. Recon gurable manufacturing systems (RMSs) [ 2, 3 ] are MSs where the components and their interaction can change over time. Thus, the structure of the system is no more static but its structure is dynamic. This recon gurability makes the system more exible, allows its adaptation for new events, and so that enhances its productivity. In a recon gurable manufacturing system, the ow changes dynamically and the components are self-recon gured to answer new requirements or to handle damages. According to [ 4 ], the RMSs guarantee three abilities in the production systems: capacity ability, functionality ability, and cost ability. Capacity ability allows the system to adapt the production's quantity to the dynamic requirement of the market. Functionality ability allows the system to change their functionality and so the quality of the product. Cost ability allows RMSs to reduce the cost of the production and the cost of the recon guration process.

Although the advantages of recon gurability in RMSs, it makes the RMSs more complex, and their development becomes a hard task. Recon gurability imposes new challenges to the developers, where new kinds of errors and anomalies will probably appear. One of the most critical questions, when designing a Recongurable Manufacturing System, is about the properties of the system after each recon guration process. When the system is recon gured, the new con guration must still satisfying the well properties satis ed in the former con guration but bad properties must be avoided. In order to guarantee such constraints, sophisticated veri cation processes are required. Veri cation of RMSs can be done using classical techniques, used for classical manufacturing systems as Petri Net (PN) [ 5 ]. This formalism attracted, early, researchers in manufacturing systems domain [ 6-9 ]. However, with its classical de nition as a non dynamic formalism (characterised by its rigid structure); this classical formalism is not suitable to catch some important aspects in RMSs as recon guration ability. To enhance Petri nets formalism, new extensions were proposed to deal with recon guration process and for the study of dynamic systems [10-14].

The global objective, of our work, is to build a formal approach that can be used to specify, simulate, and analyse recon gurable manufacturing systems. The approach uses the Recon gurable Object Nets (RONs) formalisms [15] as a formal model, exploits the RON-tool [16] to simulate interactively the system, and uses the TINA-tool (TIme Petri Net Analyzer) [17] to verify the reached con gurations. The RONs are high level Petri Nets, where the tokens can be also nets (called token-nets). The token-nets can change their structure due to reconguration rules (modelled also as other tokens called \token-rules" in the RON). The RONs formalism has two advantages; rstly it nds its mathematical background in a well-founded theory (graph transformation theory [18]), secondly it has been implemented in many automatic tools which allow the simulation and the veri cation of the system (RON-tool [16], ReConnect [ 30 ]). The current paper presents an experimentation on a case-study inspired from [19].

This paper is organised as follows: section 2 will present related work. Section 3 will detail the Recon gurable Object Nets formalism and its mathematical background in graph transformation techniques. Section 4 will present the approach proposed to specify RMSs using RONs, and then demonstrates this approach on a case study. Section 5 will treat the simulation and the veri cation processes, using automatic tools (RON-tool and TINA-tool). Finally, Section 6 will conclude this paper.

Related

Work

Several works have used PNs and their extensions in the design and veri cation of RMSs (Recon gurable Manufacturing Systems). In this section, we examine some recent works which are close to our work. We classify these works into two principal classes: works where PNs (Petri Nets), without dynamic structure, are applied to RMSs ([ 19-22, 37 ]), and works which have exploited High level Petri nets (with dynamic structure) for RMSs ([ 11, 18, 23-25, 28-30, 33- 36 ]).

The rst class of works nds its motivation in the maturity and stability of the used formalisms: p-time PNs in [20], Coloured PNs in [21], and Coloured Timed Object Nets in [19]. In this category of extensions, some researchers treated the recon guration in a modular way to facilitate the building of new models after recon guration. They enrich PNs with oriented object concepts (derivation, inheritance) or the modularity concept to overcome the recon gurability complexity. Authors of [19] used coloured timed oriented object nets (CTOONs) to facilitate recon guration of the PNs models. In CTOONs, the Petri nets models are seen as objects in classes, and where new objects can be derived from other objects. The authors of [19] consider the recon guration process in RMSs as a derivation activity in the CTOONs model. In [22], the authors proposed ITPNs (Intelligent Token Petri Nets). In the ITPNs formalism, tokens are enriched with time and knowledge. Transitions in an ITPNs model can be disabled when a token is consumed in the model. The knowledge enclosed in a consumed token decides which transitions must be disabled. A synthesis process is proposed to construct new nets from other nets. This process facilitates the de nition of new models from existing ones. However, no mechanism is included in the ITPNs to realise this recon guration. Thus, the dynamic of the structure is not implemented in the net itself. In [ 37 ], the authors used coloured timed Petri nets in the modelling of RMSs. In this work, the authors introduced a mechanism to de ne recon gurability in the CTPN formalism, yielding to a new formalism supporting recon guration. This mechanism involves recon gurable transitions, inhibitor arcs, and speci c places (machines class). However, the recon gurable mechanism is not the same used in our proposal. We believe that the recon guration in RONs is more intuitive and makes the model more expressive and more suitable for the RMSs. The power of these models [ 19-22, 37 ] resides in the existence of well-founded analysis techniques, where many properties are decidable. Many automatic tools are proposed to model, simulate and analyse systems using these formalisms. The major lack in these approaches is the absence of the ability to represent explicitly and intuitively recon guration of the system. In our work, we are interested to use formalisms where the recon guration of the system can be modelled, explicitly, through the dynamic structure of the formalism. Thus, our work can be inscribed in the second category of works.

In the second class of works, the used \Petri Net formalism" is enriched by a mechanism to recon gure itself, when necessary. Thus, the PNs model is more intuitive and more natural to support the modelling of Recon gurable Manufacturing Systems (RMSs). In this class of works, we nd several variants of extensions proposed for PN's. Each variant proposes a speci c mechanism to provide the recon guration of the PN's structure. The most popular variants nd their origins in Valk's works [ 28, 29 ] where a notion of "object token" is introduced. However this "object token", proposed by Valk, has not the ability to change its structure. The proposed extensions, for Valk's proposal, have tried to introduce recon gurability in the structure of the object nets through two basic mechanisms: graph transformation (yielding to: Recon gurable Petri Nets [ 26 ], RONs (Recon gurable Object Nets) [15], Recon gurable Petri Nets [25]), or rewriting rules (yielding to: Badouel's recon gurable Petri nets [11], Improved Net Rewriting Systems (INRSs) in [23], Hybrid Recon gurable Petri Nets (HRPNs) [24]). This recon guration expands the application of Petri Nets to several systems where the structure is dynamic. In the following paragraphs, we will highlight some works that we consider similar to our work in their objectives or in their applied techniques.

We consider that the rst work where graph transformation, as a recon gurability mechanism, was applied to PNs can be found in [18]. In this former work, graph grammars have been used to de ne the PNs transformations rules, and as an example the authors used manufacturing systems. However the aim, of this work, was not the design of"Recon gurable Manufacturing Systems", but only the re nement of Manufacturing Systems. Indeed, the objective was not to provide an approach for the speci cation and veri cation of RMSs; but only a study on the re nement of manufacturing systems, using PNs transformations.

In fact, a more close work to our work is the one proposed by Li et al. [23]. The authors developed a new formalism INRSs (Improved Net Rewriting Systems), which are based on Badouel's recon gurable Petri nets [11]. In their work, the authors proposed a hybrid approach, which combines UML.2's activity diagrams [ 32 ] and INRSs formalism, to design RMSs. We can identify three major di erences between this work and our current work. Firstly, they used the INRSs formalism which is based on the idea of "rewriting rules" proposed by Badouel [ 31 ]. However, the formalism used in our work is based on \graph transformation theory" applied to PNs [18]. This theory was proposed before \rewriting rules" and has been applied and studied in many works. Two advantages motivate the choice of graph transformation theory; the rst one is the existence of an important work in developing software tools supporting these transformations, and the second advantage can be found in the application of graph transformation theory to a variety of PNs kinds: P/T nets, Algebraic High level nets, and Coloured Petri Nets. For all these kinds of PNs, many results about properties conservation, during transformations, have been proved (a set of conserved properties during transformation can be found in [18]). The second di erence between our work and the work in [23] is that the RONs (Recon gurable Object Nets) formalism lets us make a one \connected model" which represents: (i) all the system's con gurations set, (ii) the applied transformations rules, and (iii) the dynamic at micro-level (functioning of the con guration) and the dynamic at macro-level (the recon guration in the system). All these aspects are represented in one model which is the RON-model. This is not the case in the proposed approach in [23] where an INRSs represents one con guration with its set of rewriting rule. The third di erence, and which is an important motivation in our choice, is the availability of software tools that can be used in the simulation and analysis of the RONs models (RON-tool [16], ReConNet [ 30 ]).

On another level, authors of [ 25, 33 ] applied PNs transformations techniques but for another purpose then RMSs design. In [25] the authors used Recongurable P/T nets to model mobile ad-hoc networks. The system modelled is designed for an archaeological disaster/recovery mission. In this mission, a set of teams cooperate and their behaviour can be updated to new situations. The formalism proposed, in [25], is not the same one proposed in [23]. Recon gurable P/T nets, based also on graph transformation theory, represent the building blocks of Recon gurable Object Nets which is exploited in our current work. The authors of [25] have not treated the case of manufacturing systems, and so no approach for this kind of systems was proposed; nevertheless, the dynamic aspect of their system is similar to the one presented here, because the same idea is applied: \graph transformation". In [ 34 ], the authors used Petri Nets in the development of "Dynamically Recon gurable Embedded Systems". They exploit the Petri Nets to provide a rst speci cation which will be transformed, after, to generate code. This work was interested to embedded systems (i.e. microcontrollers used in WNS) and their recon gurability rather than manufacturing systems. The formalism used is a class of basic Petri nets: Work ow PN (WFPN [ 35 ]). The recon gurability within the system is formulated as migrating of nets in the \nets-within-nets" formalism [ 36 ]. The Nets-within-nets formalism is considered as the basic of Object Petri Nets [ 36 ] used after in the proposition of RONs (used in this paper). This work deals with mobility rather than hardware recon gurability. Finally, the authors of [ 33 ] exploited the RONs formalism for the modelling of mobile agents, used in the mobile maintenance of manufacturing system. This last work used the same formalism used in our present work, but it treats also mobility rather than recon gurability.

In this paper, we propose to use the RONs formalism to specify, simulate and verify the Recon gurable Manufacturing Systems. Through an example, we present the requirements for this modelling and how the model can be constructed. One of the advantages of the RONs is the availability of dedicated automatic tools (as RON-tool used in our proposal) to simulate and analyse the constructed models. 3 3.1

Recon gurable object nets

An informal presentation

Recon gurable Object Nets (RONs) [ 26 ] was introduced rstly in [15], as High Level Nets with Nets and Rules as Tokens. In RONs, we distinguish between two levels in the Net (the system level and the token level) and two classes of tokens (token-nets and token-rules). A place in the system level can contain token-nets or token-rules. A token-net is a P/T net which can move from place to place in the system. During its moving, the token-net's marking can change as well as its structure. Transitions in the system level decide about the movement of token-nets, as well as if the marking or the structure of these token-nets will change. To change the marking of a token-net, the model must have a transition in the system level which will trigger a transition in the token-net level. However, to change the structure of a token-net, a token-rule is required to specify how this structure will be changed. Hence, the token-rule decides how the structure of the token-net will change when some transition, in the system level, is red. In RONs, recon guration of the structure concerns only the token-nets and not the whole net in the system level. This recon guration is de ned through a set of token-rules, inspired from graph transformation techniques.

Indeed, graph transformation techniques allow the formulation of two basic constructions: union and transformation, on Place/Transition Nets (P/T nets). Informally, the union construction takes two Nets N1 and N2 and yields another net N3, but the transformation construction takes one P/T net N1 and yields another net N2. In RONs formalism, these two constructions are the two basic recon gurable techniques for P/T nets. Union and transformation are based on the morphism concept de ned over P/T nets. In the following paragraphs, we will formalise the necessary concepts for our proposal: Place/Transition nets, morphisms over P/T nets, union, transformation, and nally RONs. 3.2

Place/Transition nets (P/T nets)

A place/transition net is a quadruplet (T; P; P re; P ost), where:

{ T : is a nite set of transitions; { P : is a nite set of places; { P re (for pre-domain) and P ost (for post-domain) are the two mappings de ned as: P re; P ost : T ! P The set P is the set of nite multi-sets over the set P . An element w in P can be written as the sum: w = p2P p p, where: p is a natural number ( p 2 N ). We can also consider w as a function: w : P ! N . 3.3

Morphisms over P/T nets

Given two P/T nets: N1 = (T1; P1; P re1; P ost1) and N2 = (T2; P2; P re2; P ost2). A morphism f between the two nets N1 and N2 is a function: f : N1 ! N2. We have: f = (fT ; fP ), such that: fT : T1 ! T2, and fP : P1 ! P2 are two morphisms which map transitions into transitions and places into places, respectively. fT and fP satisfy: 1. P re2 fT = fP 2. P ost2 fT = fP

P re1

P ost1

The diagram (on Figure 1) [15] summarizes the above concepts.

Based on the morphisms de ned over P=T nets, it is possible to de ne a speci c construction which is the pushout (or union) of two P=T nets. Let N1 = (T1; P1; P re1; P ost1), N2 = (T2; P2; P re2; P ost2), and I = (T0; P0; P re0; P ost0) be three P=T nets, with the two morphisms: f : I ! N1 and g : I ! N2. The net I is said a common interface between N1 and N2. The union of N1 and N2 is the Net N = (T; P; P re; P ost), de ned using the two morphisms: f 0 : N1 ! N and g0 : N2 ! N . We write: N = N1 +I N2. The operator +I is called the pushout construction (see the Figure 2) or the gluing operator. Based on the P=T gluing (or pushout) construction, the P=T transformation is constructed as a double pushout. Let L, K, R, and C be four P=T nets. A transformation f : N1 ! N2 transforms the P=T net N1 to the P=T net N2 using the rule r = (L; K; R) and the match m : L ! N1 i we have the double pushout of the Figure 3.

On Figure 3, k1, k2, m, c, and n are morphisms, thus, the P=T net C is called the context of the transformation and it satis es the following conditions: 1. TC = (T1 n mT (TL)) [ mT (k1T (TK )) ; 2. PC = (P1 n mP (PL)) [ mP (k1P (PK )) ; 3. P reC = P re1jTC (The relation P reC is the subset of P re1 which concerns only the set of transitions: TC ); 4. P ostC = P ost1jTC (The relation P ostC is the subset of P ost1 which concerns only the set of transitions: TC ); 3.6

Recon gurable object nets (RON)

A Recon gurable Object Nets (RONs) [15] is a high level net where places contain two kinds of tokens: token-nets and token-rules. Token-nets are P=T nets and token-rules are "double pushout" production rules. In the RON model, ring a transition can trigger the movement of a token-net from its current place to another place. Despite this movement, the transition can change the structure of the token-net by applying a token-rule. Indeed, a transition can transform the structure of a token-net as well as it can unify two token-nets. 4

Modelling and simulation of recon gurable manufacturing systems

4.1

The case study

Let us consider a system inspired (with some modi cations) from the one presented in [19]. This system is composed of two manufacturing cells (M C1, M C2), a storage AS=AR (Automated Storage and Retrieval System), and an AGV (Automated Guided Vehicle). The system produces a nal product A, and uses two raw materials R1 and R2 (see the Figure 4). The ow starts in M C1 and then passes to M C2.

M C1 contains a CN C (Computerized Numerical Controlled) lathe machine, a CN C milling machine, a robot, and a bu er. In M C1 (see the Figure 5), R1 and R2 start in the lathe machine then the results are processed in the milling machine. M C2 contains an assembly machine (which assembles the two products into one product A), a robot, and a bu er. The ow in M C2 is depicted on Figure 6.

Recon guration: during the life of the system, the plan will meet two recon gurations. Firstly, a new type of product is required: Product B. Product B requires the ow depicted on Figure 7, where the assembly is done before the lathe and the milling.

The second recon guration (concerns the production of B) occurs when a new cell M C3 (inspection cell) is introduced in the system (Figure 8). The inspection cell contains: a Coordinate Measuring Machine (CM M ) and a set of bu ers. 4.2

The modelling process

The modelling using RONs (Recon gurable Object Nets) requires the de nition of the two levels: System Level and Token Level. In the Token level, one must identify: the set of token-nets (the P=T nets which describe the structure and the behaviour of the manufacturing system), and the set of token-rules (production \double pushout rules" which describe the recon gurations that can be applied on the manufacturing system's structure). In the system level, places can be net-places (can contain token-nets) or rule-places (can contain token- rules). The transitions, in the system level, have the ability to trigger the transitions in a token-net, so that they change the token-net marking. In this case, the transitions (of system level) are called Fire Transitions. A second ability is to change the token-net structure by the application of a token-rule. In this case, the transitions (of system level) are called Transform Transitions. Identi cation of token-nets. In the proposed system, three tokens-nets are de ned (Figure 9, Figure 10, Figure 11). These three nets represent the three con gurations of the system, during its execution. The interpretation of the set of nodes, in these token-nets, is presented on the Table 1.

Identi cation of the token-rules. In order to simulate the recon gurations of the system, two productions rules must be de ned. A production rule will trigger a recon guration processes in the manufacturing system. The construction of these two rules requires the de nition of a set of morphisms.

Rule 1: Figure 12 depicts the rst rule. The rule contains three components: L: left, I: Interface, and R: Right. We have the rst production p = (L; I; R). In this gure: h1 and h2 are two morphisms.

On the Figure 13, we depict with more details the two morphisms h1, and h2.

Examining the Figure 13, it is easy to see that the two relations h1 and h2 are two morphisms. They satisfy the set of relations presented in the paragraph 3.3. Thus, the rst double pushout rule, which triggers the rst recon guration form token-net T N1 (Figure 9) toward the token-net T N2 (Figure 10), is depicted on Figure 14.

In Figure 14, the applications h11, h12, c, m, and g are morphisms. The net C is the context of the double pushout. Once the morphism m is de ned, the context C can be computed using the de nition presented above in the subsection (3.5). The double pushout rule is written as: r1 = (p; m), and the transformation is now written as: T N1 !(p;m) T N2.

The Figure 15 and the Figure 16 present in details the two morphisms m and g. It is also easy to verify that the two relations m and g satisfy the necessary requirements to be morphisms.

Now, we can compute the context C, using the de nition presented above in the section (3.5), thus: 1. TC = (T1 n mT (TL)) S mT (K1T (TK )) = ft11; t21; t22; t13; t23g Sft12g 2. PC = (P1nmP (PL)) S mP (K1P (PK ))) = fp11; p22; p23g Sfp1; p2; p3; p4; p12; p13g

The Figure 17 shows the context C.

Rule 2: The Figure 18 shows the second production. The second production is written: p0 = (L0; I0; R0), where: L0 for left, I0 for Interface, and R0 for Right. The two relations: h01, h02 are two morphisms.

The second double pushout rule, which triggers the second recon guration form token-net T N2 (presented in Figure 10, in the section 4.2.1) toward tokennet T N3 (presented in Figure 11, in the section 4.2.1), is depicted on Figure 19.

In the Figure 19, h011, h012, c0, m0, g0 are morphisms, and C0 is a context net. Once the morphism m0 is de ned, the context C0 can be computed using the de nition presented above in the subsection (3.5). The second double pushout rule is written as: r2 = (p0; m0), where p0 = (L0; I0; R0), and the second transformation is written as: T N2 !(p0;m0) T N3.

The system level net. In the system level, we have two kinds of transitions: Fire-Transitions which trigger the dynamic behaviour over markings of the token-nets, and Transform-Transitions which trigger the recon guration behaviour over the structure of the token-nets. Places in the system level can contain two kinds of tokens: token-nets or token-rules. A Fire-Transition takes as parameters: a net N , a transition t from this net, and updates the marking of N by ring t (if this last one is enabled). A Fire-Transition must have a guard [enabled(t) = true]. Once red, this re-transition produces a new net computed by the function: f ire(N; t).

A Transform-Transition takes as parameters: a net N , a rule r = (p; m), and applies this rule to transform N . A transform transition must have a guard [applicable(N; r)]. This Transform-Transition produces a new net with a new structure de ned by a function: transf orm(N; r).

In Figure 20, we depict the Recon gurable Object Net model for the system described in this paper. Each place (a circle) has a name (depicted in the right high side, near the circle), a type (depicted in the right low side, near the circle), and an eventually initial marking (inside the circle). Each transition (a rectangle) has a name (depicted inside the rectangle), and eventually guard (depicted outside the rectangle). An arc links a place to a transition or a transition to a place, and has a label depicted near it. 5

Simulation and veri cation

The objective of the formal modelling is to understand more the system, to simulate it and to do veri cation. In this section, we will present the simulation and veri cation processes, that can be applied in this study. We will use the automatic tool RON-Tool [16] to edit and simulate the recon guration process, and the TINA-tool [17] to verify properties of each allowable con guration obtained during the life of the system. One of the advantages when using the RONs formalism is the ability to simulate the model with the RON-tool [16]. The RONs-tool is free and can be downloaded (with its open source). The current version allows, only, the simulation of the model. The veri cation of properties is not yet implemented [16]. However, the availability of the source allows the implementation and the specialisation of the veri cation process by designers. The RONs-tool allows the graphical edition of the model. The user introduces the system net and the object nets, and the set of recon guration rules. Figure 21 shows the model of the system edited in the RONs-tool.

The interface presents three windows. The right high window depicts the system level net, the left high window depicts the object net T N1 in the place np1, and the low window depicts the transformation rule (token-rule r1) to be applied on the object net T N1. The tool can be used to simulate the behaviour of the system level net as well as the behaviour of the object nets. The TransformTransition 1 has a green colour which means that this transition can be red. 5.2

Veri cation

Besides the simulation of the models, we can verify the set of reached con gurations by the system. In this section, we propose to use the TINA-tool [17] to verify the P/T nets which model the set of con gurations. The TINA-tool (TIme Petri Net Analyser) can compute the state space graph for a Petri Net and verify many properties using this graph. Properties like: reachability, boundedness, liveness can be veri ed using TINA. Moreover the analysis using the reachability graph, the TINA-tool can do structural analysis of the net using the incidence matrix and invariants. As an example, we present the result of the TINA-tool on the rst con guration of the system: Token-net T N1 (presented in gure 9).

gure 22 shows the object net T N1 and its coverability graph computed using TINA. The proposed initial marking is two tokens in the place p11 and two tokens in the place p21.

The coverability graph can be used to verify many properties like: the live transitions and states, the dead transitions and states, the reachable states, etc. According to [18], the recon guration of P/T nets based on graph transformation preserve the liveness and the safety properties. Thus, if T N1 has some live transitions and states then these transitions and states still live in the new con guration T N2. The designer is not obliged to redo the veri cation of such properties after recon guration. 6

Conclusion

Recon gurable Manufacturing Systems (RMSs) are systems where the structure changes over time, to satisfy some new requirements or to resolve some structural problems (breakdown machines). Developing these systems and insuring their reliability become an exigency, but also a hard task. The use of formal methods, in particular Petri Nets (PNs), attracts many researchers. Many works applied PNs to specify, simulate, and verify manufacturing systems. The recon gurability aspect of RMSs presents a challenge for the use of classical Petri nets, therefore some new PNs extensions are proposed to deal with RMSs. In this paper, we have presented an experience where the Recon gurable Object Nets formalism [ 27 ] is used to specify RMSs. This formalism is based on graph transformation techniques. In this paper, we have examined (step by step) a case study, where the RMS meets two recon gurations. These two recon gurations are speci ed as two transformation-rules to be applied on the structure of the system. We have presented the nal model as a RON. After the modelling, we have presented the simulation of the model using the RON-tool [16] (to see the recon guration process) and the veri cation process of one object-net using the TINA-tool [17].

This work opens many perspectives. We propose to develop this work on three levels: (i) enrich the work and develop a concrete approach that can be used in the modelling of RMSs using RONs, (ii) working on the RONs automatic tool (open source), to implement properties veri cation processes, and nally (iii) introducing the time factor in the modelling process. The amelioration of the e ciency (reducing the global time of the manufacturing process) of the system is one of the most motivation of recon guration. This e ciency can be veri ed by the use of temporal model. Time Petri Nets [ 27 ] can be used for this purpose; however recon guration is not yet well de ned for time Petri Nets. One important perspective can be the work on recon guration of Time Petri Nets. [10] Valk, R.: Self-modifying nets, a natural extension of petri nets. In: Proceedings of the Fifth Colloquium on Automata, Languages and Programming 1978; 1721 July 1978; Udine, Italy: LNCS 62. 464-476 (1978) [11] Badouel, E., Llorens, M., Oliver, J.: Modelling Concurrent Systems: Recon gurable Nets. In Proceeding of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'03) 2003, 23-26 June 2003; Las Vegas, Nevada, USA. pp. 1568-1574 (2003) [12] Valk, R.: Petri Nets as Token Objects: An Introduction to Elementary Object Nets. In: Applications and Theory of Petri Nets ICATPN'98; June 1998; Lisbon, Portugal: LNCS 1420. pp. 1{25 (1998) [13] Lomazova, IA.: Nested Petri Nets: Multi-level and Recursive Systems. Fundamenta

Informaticae. 47, 283{293 (2001) [14] Asperti, A., Busi, N.: Mobile Petri Nets. Mathematical Structures in Computer

Science. 19, 1265{1278 (2009) [15] Ho mann, K., Ehrig, H., Mossakowski, T.: High-Level Nets with Nets and Rules as Tokens. In: Proceedings of the 26th international conference on Applications and Theory of Petri Nets; 20-25 June 2005; Miami, USA: LNCS 3536. pp. 268288 (2005) [16] Biermann, E., Ermel, C., Hermann, F., Modica, TA.: Visual Editor for Recon gurable Object Nets based on the ECLIPSE Graphical Editor Framework. In: Proceeding of the 14th Workshop on Algorithms and Tools for Petri Nets (AWPN2007); 20-21 September 2006; Koblenz, Germany. pp. 1-6 (2007) [17] Berthomieu, B., Ribet, PO., Vernadat, F.: The tool TINA construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research. 42, 2741{2756 (2004) [18] Ehrig, H., Padberg, J.: Graph Grammars and Petri Net Transformations. In: Desel, Jrg; Reisig, Wolfgang; Rozenberg, Grzegorz, editors. Lectures on Concurrency and Petri Nets: Advanced Course PNT, 2004; Springer Berlin Heidelberg. pp. 496-536 (2004) [19] Meng, X.: Modeling of recon gurable manufacturing systems based on colored timed object-oriented Petri nets. Journal of Manufacturing Systems. 29, 81-90 (2010) [20] Julia S., de Oliveira, FF., Valette, R.: Real time scheduling of Work ow Management Systems based on a p-time Petri net model with hybrid resources. Simulation Modelling Practice and Theory. 16, 462-482 (2008) [21] Cunha de Aguiar, AJ., Villani, E., Junqueira, F., Coloured Petri nets and graphical simulation for the validation of a robotic cell in aircraft industry. Robotics and Computer-Integrated Manufacturin. 27, 929-941 (2011) [22] Wu, N., Zhou, M.: Intelligent token Petri nets for modelling and control of recongurable automated manufacturing systems with dynamical changes. Transactions of the Institute of Measurement and Control. 33, 9-29 (2009) [23] Li, J, Dai, X, Meng, Z, Dou, J and Guan, X, (2009). Rapid design and recon guration of Petri net models for recon gurable manufacturing cells with improved net rewriting systems and activity diagrams. Computers & Industrial Engineering, 57(4) 14311451. [24] Lejri, O., Tagina, M.: Hybrid Recon gurable Petri Nets for modelling Hybrid Recon gurable Manufacturing Systems. Journal of Studies on Manufacturing. 1, 7584 (2011) [25] Prange, U., Ehrig, H., Ho mann, K., Padberg, J.: Transformations in Recon gurable Place/Transition Systems. In: Degano P, Nicola RD, Meseguer J, editors. Concurrency, Graphs and Models 2008, LNCS 5065, Springer Berlin Heidelberg. pp. 96-113 (2008)

References

[1] Serope , K. , Schmid , S. : Manufacturing, Engineering & Technology. 6th ed. Prentice Hall ( 2009 )

[2] Mehrabi , MG. , Ulsoy , AG., and Koren Y.: Recon gurable manufacturing systems: key to future manufacturing . Journal of Intelligent Manufacturing . 11 , 403 - 419 ( 2000 )

[3] Katz , R. : Design principles of recon gurable machines . The International Journal of Advanced Manufacturing Technology . 34 , 430 - 439 ( 2007 )

[4] Korena , Y. , Shpitalni , M. : Design of recon gurable manufacturing systems . Design of recon gurable manufacturing systems . 29 , 130 - 141 ( 2010 )

[5] Murata , T. : Petri nets: Properties, analysis and applications . Proceedings of the IEEE . 77 , 541 - 580 ( 1989 )

[6] Valette , R. , Cardoso , J. , Dubois , D. : Monitoring manufacturing systems by means of Petri nets with imprecise markings . In: IEEE 1989 International Symposium on Intelligent Control; 25 - 26 September 1989; Albany, NY , USA. pp. 233 - 238 ( 1989 )

[7] Zhou , MC. , Mcdermott , K. , Patel , PA.: Petri net synthesis and analysis of a exible manufacturing system cell . IEEE Transactions on Systems, Man and Cybernetics . 23 , 523 - 531 ( 1993 )

[8] Cheng, CW., Sun , TH., Fu , LC.: Petri-net based modeling and scheduling of a exible manufacturing system . In: IEEE 1994 International conference on robotics and automation; 8-13 May 1994 ; San Diego, CA. 513 - 518 ( 1994 )

[9] Wang , LC.: Object-oriented Petri nets for modeling and analysis of automated manufacturing systems . Computer Integrated Manufacturing Systems . 9 , 111 - 125 ( 1996 )

[26] Biermann , E. , Modica , T. : Independence Analysis of Firing and Rule-based Net Transformations in Recon gurable Object Nets . Electronic Communications of the EASST . 10 1 - 13 , ( 2008 )

[27] Merlin , PM. , Farber , DJ.: Recoverability of communication protocols: Implications of a theoretical study . IEEE Transactions on Communication . 24 , 10361043 ( 1976 )

[28] Valk , R. : Petri Nets as Token Objects: An Introduction to Elementary Object Nets , Proc. of the International Conference on Application and Theory of Petri Nets, LNCS 1420 , pages 125 , ( 1998 )

[29] Valk , R. : Concurrency in Communicating Object Petri Nets , In G. Agha, F. de Cindio, and G. Rozenberg, editors, Concurrent Object-Oriented Programming and Petri Nets , LNCS 2001 , pages 164 { 195 . Springer. ( 2001 )

[30] Ede , M. , Ho mann , K. , Oelker , G. , Padberg , J.: RECONNET: A Tool for Modeling and Simulating with Recon gurable Place/Transition Nets , Electronic Communications of the EASST 7th International Workshop on Graph Based Tools , (GraBaTs 2012 ), Vol. 54 , ( 2012 ).

[31] Badouel , E. , Oliver , J.: Recon gurable Nets, a Class of High Level Petri Nets Supporting Dynamic Changes within Workow Systems , INRIA report N 3339 , ( 1998 )

[32] U2 Partners , Uni ed Modeling Language: Superstructure, version 2 .0, 3rd revised submission to OMG RFP ad/00-09-02, http://www.omg.org/cgi-bin/doc?ad/2003- 04-01, April 2003 .

[33] Abid , K. , Kahloul , L. , Mous , LH., Kazar , O. : Formal Speci cation of a Mobile Agent Based Maintenance for Manufacturing Systems . In the 7th International Workshop on Veri cation and Evaluation of Computer and Communication Systems. Florence, Italy, November 21-22 , 2013 .

[34] Richta , T. , Janouek , V. , Ko , R.: Petri Nets-Based Development of Dynamically Recon gurable Embedded Systems. In proceeding of Petri Nets and Software Engineering . pp. 203218 . ( 2013 ).

[35] Aalst , VD. Hee, KV.: Work ow Management: Models, Methods, and Systems . IT press, Cambridge, MA. ( 2002 ).

[36] Valk , R. : Object Petri Nets Using the Nets-within-Nets Paradigm . In: Jrg Desel, Wolfgang Reisig, and G.R . (ed.) Advances in Petri Nets: Lectures on Concurrency and Petri Nets , volume 3098 of Lecture Notes in Compu ter Science . pp. 819 - 848 . Springer-Verlag, Berlin, Hei- delberg, New York, New York, USA. ( 2004 )

[37] Zhang , L. , Rodrigues , B. : Modeling Recon gurable Manufacturing Systems With Colored Timed Petri Nets . International Journal of Production Research . 47 , 4569 - 4591 ( 2009 )

[38] Koren , Y. , Heisel , U. , Jovane , F. , Moriwaki , T. , Pritschow , G. , Ulsoy , G. , Brussel, HV.: Recon gurable manufacturing systems . CIRP Annals - Manufacturing Technology . 48 , 527 - 540 ( 1999 )