Object-oriented Petri nets and π -calculus-based modeling and analysis of reconfigurable manufacturing systems

Abstract

Reconfigurable manufacturing systems can change the structure of the systems to cope with manufacturing market requirements. Reconfigurability brings about new challenges for reconfigurable manufacturing systems’ development. In order to describe, analyze, and verify the reconfiguration of reconfigurable manufacturing systems, a reconfigurable manufacturing system formal model is proposed from the perspective of multi-agent systems, in which two complementary formalisms, namely, object-oriented Petri nets and π-calculus, are employed as formalisms. The object-oriented Petri nets are utilized to model the initial structure as well as system behaviors of reconfigurable manufacturing systems, while π-calculus is adopted to describe the reconfiguration of reconfigurable manufacturing systems. Some supporting tools of Petri nets and π-calculus can be used to analyze, verify, and validate the reconfigurable manufacturing system formal model. The reconfigurability mechanism and consistency of reconfigurable manufacturing systems can also be analyzed by π-calculus.

Keywords

Reconfigurable manufacturing systems formal method Petri net reconfigurability

Introduction

Driven by a highly volatile market, traditional manufacturing systems have to improve the capacity to meet the new requirements. In recent years, an automated manufacturing system (AMS) has emerged as a new pattern of manufacturing systems, which is a computer-controlled system revealing a high level of resource sharing.¹ It consists of a set of interconnected workstations and material handling systems, and different types of parts can be processed based on the prescribed sequences of operations. In order to further improve the flexibility and productivity, flexible manufacturing systems (FMSs)² and reconfigurable manufacturing systems (RMSs)³ have been developed. They are new types of AMSs.

In contrast to traditional manufacturing systems, RMSs can change the components, interactions, and structure over time and can be rapidly changed from one production mode to another to produce new products within the same product family.⁴ A typical RMS consists of reconfigurable machine tools (RMTs), computerized numerical controlled (CNC) machines, robots, automated guided vehicles (AGVs), and input/output buffers.

The reconfigurability of an RMS makes it more flexible to adapt to the market demand changes through addition, removal, update, or adjustment of new machines or components.⁵ Although the advantages of reconfigurability make it more capable and productive, its development becomes a challenging issue. The difficulties of developing an RMS are how to create and verify its initial configuration formal model and how to describe, analyze, and verify the reconfiguration.⁵ Modeling of reconfigurable manufacturing system plays a key role in its efficient design. Traditional validation techniques, such as computer simulation and software testing, cannot sufficiently verify the correctness of a system.⁶ Formal methods can accurately describe, analyze, and verify complex systems with mathematical methods and supporting tools, which allow one to detect bugs at the modeling phase and repair them at the high level, where changes are easily made.⁷ Consequently, the use of formal methods for RMS development is indispensable.⁵

Researchers have presented many formal methods for modeling and analyzing AMSs. Petri nets and their extensions are the most competent tools for modeling them.^8–10 Li and Zhou¹¹ present elementary siphons to solve deadlock prevention problems in FMSs’ modeling, and then they propose an algorithm to obtain a set of elementary siphons and apply it to FMSs’ modeling. Wu et al.¹ model each resource in AMSs with a single place and then propose the resource-oriented Petri nets to model AMSs and solve the deadlock avoidance problems. Most existing researches focus on modeling FMSs using Petri nets and use deadlock resolution methods to prevent or avoid deadlocks in FMSs. For RMSs’ modeling and analysis, it is a challenge to how to deal with its reconfigurations. Meng¹² uses colored timed object-oriented Petri nets (OPNs) to describe the reconfiguring process of a manufacturing system and develops a modular hierarchical structure of RMSs. The reconfiguration is depicted as the inheritance of Petri net models. Wu and Zhou¹³ propose an intelligent token Petri net (ITPN) to model and control RMSs. Tokens in ITPN represent job instances which carry real-time knowledge describing the system status and reconfigurations. ITPN models RMSs in a modular way. Only the changed part model will be modified when changes in RMSs occur. However, the reconfiguration mechanism in ITPN needs to be further studied. De Silva et al.¹⁴ propose reconfiguration mechanisms using holonic and multi-agent system (MAS) techniques and then use Petri nets to describe the combined top–down and bottom–up approach. However, the reconfiguration is not addressed by Petri nets. Tarnauca et al.¹⁵ introduce reconfigurable finite capacity Petri nets (RFCPNs) to describe an FMS. The changes in the FMS are modeled by adding or removing arcs or by setting different place capacities. Li et al.¹⁶ present an improved net rewriting system (INRS)–based method for automatic reconfiguration of Petri net supervisory controllers for RMS. INRS can describe the variations in the structure of Petri nets. Thus, it can overcome the limitations of the net rewriting system and also keep its important behavioral properties unchanged. Li et al.⁵ also combine INRS with UML 2 activity diagrams to design RMSs. Kahloul et al.¹⁷ use reconfigurable object nets (RONs) to model, simulate, and analyze RMSs. The reconfiguration in RONs is specified as graph transformation theories. Some RON tools are used to simulate and analyze RMS models. All the above work has tried to model and analyze RMSs. Nevertheless, most of them fail to analyze or verify the reconfiguration results. Software supporting tools have not been developed for most of Petri net extensions.

No single formal method seems to be suitable for modeling and analyzing every aspect of RMSs. This work integrates OPNs and π-calculus to specify and analyze RMSs. Then an reconfigurable manufacturing system formal model (RMSFM) is proposed from MAS point of view, where OPNs are used to describe the static structure and behaviors of RMSs, and π-calculus is employed to characterize manufacturing configuration changes (reconfigurations). We can use some well-established techniques, such as reachability tree method, matrix-equation approach, and model checking, to analyze, verify, and validate RMSFM with respect to certain desired properties. Therefore, the design errors in the system modeling process can be detected and fixed at the model level, where changes are easier and cheaper to make. RMS control systems can be designed directly from RMSFM specifying the control logic of RMSs.

OPNs and π-calculus

Petri nets are an excellent graphical modeling tool that can depict the static structure and behaviors of a system. They can model causality and concurrency of a system. Furthermore, some structural objects and mathematical analysis methods can be employed to analyze, verify, and validate the system. Petri nets have been widely applied to discrete event systems, supervisory control theory, and the short-term scheduling problem.^18–23 The ordinary Petri nets, however, do not address the modeling issues of dynamic structures.

π-Calculus is suitable for describing concurrent systems whose structures may change during the run-time. It uses algebraic operators to model a complex system.²⁴ However, π-calculus is too complicated to be easily used by non-technical users, and it has limited supporting tools only.

The modeling capabilities of Petri nets and π-calculus are different such that we cannot make full use of their advantages if they are employed separately to describe a system. Therefore, a practical approach is to use Petri nets and π-calculus in combination. The combination keeps the advantages of both the specification formalisms. Petri nets can be employed to depict the system static structure and behaviors, while π-calculus can be used to describe the system dynamic changes. According to the system requirements, we can use different kinds of Petri nets and π-calculus.

OPNs

The ordinary Petri nets lack modularity, reusability, and maintainability and are highly system dependent. To improve the modeling capability of ordinary Petri nets, OPNs are proposed by combining Petri nets with object-oriented theory.²⁵ OPNs promote better understanding for a complex system. In our previous work,^26,27 we present a new kind of OPNs from software components’ perspective. The branch bisimilarity of OPNs is proposed to decide the behavior equivalence, and the object-oriented characteristics, such as encapsulation, inheritance, and polymorphism, are analyzed. This work revises our previous OPNs’ definition. The formal definition of a physical object can be given as follows.

Definition 1

A physical object model OPN is a tuple $OPN = (Σ, P, T, F, E, G, C)$ , where

$Σ$ is a color set, which is a finite set of data types, variables, and functions.

P is a finite set of places, $P = {p_{1}, p_{2}, \dots, p_{j}}$ .

$T = T_{o} \cup IT \cup OT$ ; $T_{o}$ is a finite set of ordinary transitions, $T_{o} = {t_{o 1}, t_{o 2}, \dots, t_{ok}}$ ; IT (input transition) and OT (output transition) are sets of input and output transitions which represent the input and output interfaces, $IT = {i t_{1}, i t_{2}, \dots, i t_{l}}$ and $OT = {o t_{1}, o t_{2}, \dots, o t_{m}}$ .

$F \subseteq (P \times T) \cup (T \times P)$ is an arc set connecting transitions and places.

$E : F \to expression$ denotes an arc expression function.

G is a guard function that is defined from T into expressions such that $\forall \in T : [Type (G (t)) = Bool \land Type (Var (G (t))) \subseteq Σ]$ .

$C (P) \subseteq Σ$ is a set of colors associated with places P.

A system is composed of objects and their interconnection relations, and its formal definition is given as follows.

Definition 2

A system S is a three-tuple $S = (O, Gate, C)$ , where

O is a finite set of physical objects in the system, $O = {OP N_{1}, OP N_{2}, \dots, OP N_{i}}$ .

Gate is a finite set of communication places denoted by eclipses, which is applied to message passing among OPN.

$C (Gate) \subseteq Σ$ is a set of colors associated with Gate.

π-Calculus

π-Calculus²⁸ is a concurrent systems’ computation model. It is suitable for describing a system whose structure is continually changing. The most primitive entities in π-calculus are name and process. Names can be defined as an infinite set $X$ , which is $x, y, \dots \in X$ . The names represent channels, variables, or constants. A process is regarded as an abstraction of a thread. Processes can be defined as $P, Q, \dots \in P$ , which can be built from names by π-calculus syntaxes. Processes interact with each other by channels.

The syntaxes of processes can be shown as follows²⁸

\begin{matrix} P : : = 0 \\ | P_{1} + P_{2} \\ | \bar{y} x . P \\ | y (x) . P \\ | τ . P \\ | P_{1} | P_{2} \\ | (ν x) P \\ | [x = y] P \\ |! P \end{matrix}

0 denotes that process P does nothing, which is called inaction.

$P_{1} + P_{2}$ denotes that the behaviors of process P like either $P_{1}$ or $P_{2}$ .

$\bar{y} x .$ is a negative prefix. $\bar{y} x . P$ denotes an output port of process P which can send the name x and then behaves like P.

$y (x) .$ is a positive prefix. $y (x) . P$ denotes an input port of process P which can receive another name z to replace name x and then behaves like P.

$τ$ is a silent prefix, denoting that process P does not interact with the other processes.

$P_{1} | P_{2}$ denotes that $P_{1}$ and $P_{2}$ run in parallel.

$(ν x) P$ denotes that x is a local name in P, which cannot be used as a channel to interact with other processes.

$[x = y] P$ denotes that the process behaves like P if x matches y. If not, it behaves like 0.!

$P$ denotes that an infinite number of replications of P run in parallel.

Example 1

Link passing is the basic example of the π-calculus, which is shown in Figure 1. Suppose that the server S interacts with printer P via a link y and then passes y by link x to client C. C is willing to receive it to print data d. Thus, S may be $S = \bar{x} y . S'$ , C may be $C = x (z) . \bar{z} d . C'$ , and P may be $P = y (α) . P'$ . In this case, the transition is

\begin{matrix} \bar{x} y . S' | x (z) . \bar{z} d . C' | y (α) . P' \\ \overset{τ}{\to} S' | \bar{y} d . C' | y (α) . P' \\ \overset{τ}{\to} S' | C' | P' {d / α} \end{matrix}

(1)

Figure 1.

Link passing.

The link x between server S and printer P is public in Figure 1. Now suppose that the link x is private. The privacy of x should be denoted by a restriction. Therefore, the transition will become

\begin{matrix} (ν x) (\bar{x} y . S' | x (z) . \bar{z} d . C') | y (α) . P' \\ \overset{τ}{\to} (ν x) (S' | \bar{y} d . C') | y (α) . P' \\ \overset{τ}{\to} (ν x) (S' | C') | P' {d / α} \end{matrix}

(2)

π-Calculus defines structural congruence, reduction rules, strong bisimulation, and strong bisimilarity to analyze a system. π-Calculus has been widely applied to mobile communication systems, computer networks, and software engineering. To improve π-calculus modeling capability, some extensions are proposed, such as polyadic π-calculus.²⁹

Formal modeling of reconfigurable manufacturing systems

To respond efficiently and effectively to dynamic changes in RMSs, the manufacturing control systems with intelligence, robustness, and adaptation need to be developed. MASs are one of the subfields in distributed artificial intelligence, which are suitable for building intelligent and distributed systems. An agent can be regarded as an autonomous system. Agents can work together to accomplish a common goal. Agents have been used to study reconfiguration systems.^30,31 Consequently, MASs can be introduced into RMSs to implement some important properties, such as autonomy, responsiveness, reconfigurability, and openness. In an RMS, agents can express physical manufacturing units (e.g. machines, robots, buffers, and auto-guided vehicles) as well as products and logical objects. MASs can help RMSs to respond quickly to reconfigurations and disturbances through decision-making.

In this work, we use agents to represent machines, robots, and buffers in an RMS and then illustrate the usefulness and applicability of OPNs and π-calculus to the specification of the RMS. First, we employ OPNs to specify the static structure of the RMS and then π-calculus is used to depict the reconfiguration of the RMS. Finally, an RMSFM is proposed. It is built to guide the development of RMSs from the high level. We can also use mathematical methods and tools to analyze and verify the formal models. Therefore, some problems can be detected and fixed at the model level.

Definition 3

RMSFM is a two-tuple, $RMSFM = (SM, DM)$ , where SM is a static model of an RMS and DM is a reconfiguration model of the RMS.

Static model of RMSs

The static model of an RMS SM is a two-tuple, $SM = (EA, CA)$ , where $EA = (E A_{1}, E A_{2}, \dots, E A_{α})$ is a finite set of entity agents, such as robot agents and machine agents; $CA = (C A_{1}, C A_{2}, \dots, C A_{β})$ is a finite set of connecting agents which connect different entity agents.

Entity agent

Entity agents can be classified as reacting agents or hybrid agents according to their function. The reacting agent formal model is shown in Figure 2, which is modeled by OPNs. The transitions IT and OT describe the interfaces of the reacting agent. $P_{r}$ is an abstract place denoted by an eclipse, which represents the condition/action rules and can quickly respond to the changes in environments.

Figure 2.

The reacting agent model.

The hybrid agent formal model is shown in Figure 3, which is described by OPNs. The hybrid agent integrates the reactive model with belief–desire–intention (BDI) model,³² where $P_{d}$ , $P_{r}$ , $P_{k}$ , $P_{g}$ , and $P_{p}$ are the abstract places denoted by shaded eclipses. $P_{d}$ , $P_{r}$ , $P_{k}$ , $P_{g}$ , and $P_{p}$ are defined as follows:²⁶

$P_{d}$ is a decision-making module which dispatches the message to the reactive module or BDI module.

$P_{r}$ is a reactive module which represents the agent can use the IF–THEN rules saved in the knowledge base to make quick response to the environment.

$P_{k}$ is a knowledge base module corresponding to the beliefs in the BDI model, which describes the environment and the IF–THEN rules.

$P_{g}$ is a goal module corresponding to the desires in the BDI model, which represents the desired states.

$P_{p}$ is a plan module corresponding to the intentions in the BDI model, which represents a set of plans.

Figure 3.

The hybrid agent model.

The abstract places can be refined according to the requirements. The entity agents interact with each other using their interfaces. Their internal implementation is invisible for other agents so as to keep well encapsulation.

Connecting agent

The connecting agent is a communication facilitator defining the interaction rules and transmitting the interaction information. The connecting agent coordinates and supervises entity agents.

A connecting agent may be $C A_{β} = (Gate, KB, RL)$ , where

Gate is the tuple in OPN model and represents the channels among agents.

KB represents knowledge base and stores the information of entity agents and the external environment information.

RL is a set of entity agent identifiers, which is defined as $RL = {AI D_{1}, \dots, AI D_{n}}$ .

The static model of RMSs is assembled by the entity agents and connecting agents. In Figure 4(a), an RMS is composed of connecting agents and some entity agents; in Figure 4(b), a large-scale RMS is composed of some subsystems which are connected by the connecting agents.

Figure 4.

The communication model of RMSs.

Example 2

Let us consider a simple RMS. It consists of one lathe machine, one milling machine, one robot, and one buffer. The robot is responsible for loading or unloading parts from the machines and buffers.

We use entity agents to represent the robot, lathe machine, milling machine, and buffers. According to their functions, the robot, lathe, and milling machine can be regarded as hybrid agents, and buffers are represented as reacting agents. Using the appropriate agent models, individual machines and robot agents can make their own decisions relating to resource allocation and coordination. These entity agent formal models in the RMS are shown in Figure 5. The lathe and milling machine models can be refined with the machine model according to the specifications.

Figure 5.

Entity agent formal models in the RMS.

The abstract RMS formal model is shown in Figure 6. The robot, machine, and buffer agents interact with each other by the communication places Gate. Figures 5 and 6 illustrate the static model of the RMS, which is described by Petri nets.

Figure 6.

The abstract RMS formal model.

Reconfiguration model of RMSs

To meet new product requirements, some new machines may join RMSs. If the machines or robots in RMSs have some faults, they need to update. Therefore, RMSs need to be reconfigured to meet the market or environment requirements. The reconfiguration model DM employs π-calculus to describe the typical reconfiguration processes, such as the addition or removal of entity agents, update of entity agents, and adjustment of logic relationship among entity agents.

Addition or removal of entity agents

Machines, robots, and buffers are represented as the entity agents. When a new entity agent, such as a new machine, is added into RMSs, it needs to register its information in a connecting agent. The addition process of an agent is

NewMachine (id, s) = Add (id, s)

(3)

It means that a new machine is added with identifier id and function s which consists of the name and capability. The register process of the new machine agent is

MachineReg (id, s) = (ν id, f) (\bar{register} 〈 id, s 〉)

(4)

It means that the machine agent sends identifier id and function s through the channel register to the connecting agent. The corresponding register process in the connecting agent is

CAReg (x, y) = (ν a, b) (register (a, b))

(5)

It means that the connecting agent receives the new function by the channel register, and a and b are the private names. When some new products need to be produced, the operator wants to check the functions of the machines to make some decisions to respond to the requirements. The operator seeks the functions provided by different machines using a connecting agent. The connecting agent searches from its knowledge database to seek a required agent. If the agent providing the functions is found, the connecting agent builds the interactive channels for these agents to produce the new products; if not, the functions can be subscribed. The connecting agent will notify the operator when a required agent registers. This requesting process of the operator is

\begin{matrix} RequireFunction (i, r, l) \\ = \bar{i} 〈 a 〉 . r (z) . ([z = nil] . \bar{subscribe} 〈 a 〉 + \bar{z} 〈 l 〉) \end{matrix}

(6)

The operator sends request a via i to search the agent providing the functions and then waits for a response by channel r. When the operator gets the identifier of the corresponding agent z, the operator sends the requiring address l to the service agent via z.

The functions’ query process is

\begin{matrix} QueryFunction (i, r, p) = i (y) . (\bar{kb} 〈 y 〉 | Belief (y)) \\ . (\bar{r} 〈 nil 〉 . subscribe (y) + \bar{r} 〈 p 〉) \end{matrix}

(7)

The connecting agent receives request y by i and judges whether function a exists. If function a exists, the agent identifier p is transmitted through channel r; otherwise nil is transmitted and this service is subscribed.

The corresponding process in the agent providing the functions is

ProvidFunction (p, s) = p (x) . \bar{x} 〈 s 〉

(8)

The agent providing the function sends service s by channel x to the operator. The entire dynamic process of the function requiring and providing is described as follows

RequireFunction (i, r, l) | QueryFunction (i, r, p) |

\begin{matrix} ProvidFunction (p, s) \\ = \bar{i} 〈 a 〉 . r (z) . ([z = nil] . \bar{subscribe} 〈 a 〉 + \bar{z} 〈 l 〉) | i (y) . (\bar{kb} 〈 y 〉 | \\ Belief (y)) . (\bar{r} 〈 nil 〉 . subscribe (y) + \bar{r} 〈 P 〉) | p (x) . \bar{x} 〈 s 〉 \\ \overset{τ}{\to} r (z) . ([z = nil] . \bar{subscribe} 〈 a 〉 + \bar{z} 〈 l 〉) | (\bar{kb} 〈 a 〉 | \\ Belief (a)) . (\bar{r} 〈 nil 〉 . subscribe (y) + \bar{r} 〈 P 〉) | p (x) . \bar{x} 〈 s 〉 \\ \overset{τ}{\to} r (z) . ([z = nil] . \bar{subscribe} 〈 a 〉 + \bar{z} 〈 l 〉) | \bar{r} 〈 P 〉 | p (x) . \bar{x} 〈 s 〉 \\ \overset{τ}{\to} \bar{p} 〈 l 〉 | p (x) . \bar{x} 〈 s 〉 \\ \overset{τ}{\to} \bar{l} 〈 s 〉 \end{matrix}

According to the above process, the interactive channel between two agents is built. When a machine agent or robot agent breaks down, damages, or achieves its goal, it has to be removed from the RMS. Therefore, its information must be deleted from the corresponding connecting agent. The removal process of an agent is

AgentRemove (id, f) = Delete (id, f)

(9)

It means that an agent with an identifier id and a function f is deleted.

Update of entity agents

Some entity agents such as machines and robots may break down or provide some new functions to respond to new requirements, so they need to upgrade. The entity agent update can be classified into two categories:²⁷

Holding semantic update: the control algorithms of an agent in RMSs may make some errors or low efficiency, so the agent must be updated.

Extended semantic update: for new product requirements emerge, an agent with new functions will replace the former agent in RMSs.

For the holding semantic update, we can use the weak equivalent in π-calculus to determine whether the new agent replaces the former agent. If their behaviors are equivalent, the new agent can replace the former one and the environment does not apperceive the substitution. The holding semantic update can be defined as follows.

Rule 1

Suppose that the behaviors of agents $Agen t_{0}$ and $Agen t_{1}$ are processes P and Q, respectively. If $P \approx Q$ , $Agen t_{1}$ can update $Agen t_{0}$ denoted as $P ▹ Q$ , which is called the holding semantic update.

Holding semantic update means that the internal algorithms in RMS control systems are only updated, while their interfaces and external behaviors are not changed.

For the extended semantic update, a more powerful agent replaces the former agent. The extended semantic update can be defined as follows.

Rule 2

Suppose that the behaviors of agents $Agen t_{0}$ and $Agen t_{1}$ are processes P and Q, respectively. P and Q satisfy the following conditions:

$fn (P) \subseteq fn (Q)$ .

If $P \overset{τ}{\to} P'$ , then $\exists Q', Q \Rightarrow Q'$ .

If $P \overset{x (z)}{\to} P'$ , then $\exists Q', Q \overset{x (z) \dots x_{i} (z_{i})}{\to} 2.3 pc Q'$ $(\overset{x (z) \dots x_{i} (z_{i})}{\to} 2.5 pc$ means that Q can execute the other actions $x_{i} (z_{i})$ except $x (z))$ .

If $P \overset{\bar{x} 〈 y 〉}{\to} P'$ , then $\exists Q', Q \overset{\bar{x} 〈 y 〉 \dots {\bar{x}}_{i} 〈 y_{i} 〉}{\to} 2.6 pc Q'$ $(\overset{\bar{x} 〈 y 〉 \dots {\bar{x}}_{i} 〈 y_{i} 〉}{\to} 2.5 pc$ means that Q can execute the other actions ${\bar{x}}_{i} 〈 y_{i} 〉$ except $\bar{x} 〈 y 〉))$ .

If $P \overset{\bar{x} y}{\to} P'$ , then $\exists Q', Q \overset{\bar{x} y \dots {\bar{x}}_{i} y_{i}}{\to} 2.1 pc Q'$ .

Then Q updates P; therefore, $Agen t_{1}$ can update $Agen t_{0}$ denoted as $Agen t_{1} ▹ ▹ Agen t_{0}$ , which is called the extended semantic update. In Condition 1, the freedom name set of P is the subset of the freedom name set of Q; Condition 2 shows that if P can reach $P'$ by executing an internal action, Q can reach $Q'$ by executing at least an internal action; Conditions 3–5 show that Q can respond to the actions of P; it can also execute new actions.

Extended semantic update means that the new agent in RMS control systems may provide new functions and interfaces to improve the system performance. RMSs can meet the new product requirements by the entity agent update and exhibit these capabilities of responsiveness, flexibility, and reconfigurability.

Adjustment of logic relationship among entity agents

To respond to the new product requirements, the operating sequences of the machine agents may be adjusted. Given that $agen t_{1}$ interacts with $agen t_{2}$ via channel $G_{1}$ (denoted as x), and $agen t_{2}$ interacts with $agen t_{3}$ via channel $G_{2}$ (denoted as y) to produce part A. Now we need to use $agen t_{1}$ and $agen t_{3}$ to produce part B. Therefore, $agen t_{1}$ needs to switch its channel to $agen t_{3}$ . The adjustment of logic relationship is shown as follows

(ν x) (\bar{y} 〈 x 〉 \cdot a g e n t_{2} | a g e n t_{1}) | y (z) \cdot a g e n t_{3} \overset{τ}{\to} (ν x) (a g e n t_{2} | a g e n t_{1}) | a g e n t_{3} {x / z}

It means that before $agen t_{2}$ removing, the private channel x is transferred to $agen t_{3}$ . Therefore, $agen t_{3}$ can interact with $agen t_{1}$ via channel x.

Analyzing reconfiguration of reconfigurable manufacturing systems

For analyzing the formal model of RMSs, the related methods and supporting tools can be employed to analyze the deadlock, boundness, and reachability of the model. Petri nets provide some mathematical analysis methods and techniques to verify the logic correctness of the static model SM, and π-calculus can analyze and verify the reconfiguration model DM.

In this section, the major attention focuses on analyzing the reconfigurability of RMSs using π-calculus, especially the consistency of the agents. The reconfiguration makes RMSs more flexible to enhance the productivity. The machine, robot, and buffer agents in RMSs have to communicate and collaborate in order to achieve a goal. The success of RMSs depends on the quality of agents and their interactions.¹⁷ The consistency can ensure the successful interactions among agents in RMSs.

The compatibility of the internal implementations and interfaces in agents

An agent is composed of the interfaces and internal implementations in RMSs. Machine agents, robot agents, and buffer agents interact with each other by the interfaces. Interfaces specify the functions of the agents. The internal implementations of the agents must be compatible with their interfaces. Therefore, the agents execute the behaviors specified by the interfaces. To analyze the compatibility between the interfaces and the internal implementations, the name hiding of π-calculus is used to describe the compatibility.³³

Suppose that a process P and a set of names $N \subseteq fn (P)$ , $P / N$ represents the process hides the names belonging to N in P

P / N = (ν N) (P | \underset{n \in N}{Π} Hide (n))

(10)

where $Hide (n) = n (m) . (Hide (n) | Hide (m)) + (ν m) (\bar{n} 〈 m 〉 . (Hide (n) | Hide (m)))$ .

For each name $n \in N$ , process $Hide (n)$ hides it in P. $Hide (n)$ means that it always performs input and output actions along n. Therefore, the behavior is predigested to the internal behavior $τ$ so as to hide the name n.

The hide names are distinct with the restricted names. The restricted names cannot interact with the other processes, but they can be regarded as values to be transmitted to the other processes. The hide names mean that the freedom names in processes are hidden and the actions along them are regarded as silent actions $τ$ .

Definition 4

(Agent interface) Suppose an entity agent AComp and a process P, if

fn (P) \subseteq fn (AComp) and P \approx AComp / (fn (AComp) - fn (p))

(11)

then P is called an interface in AComp.

Definition 4 means that the actions executed by interface P is a subset of internal implementations in the agent AComp. Therefore, the freedom names of the interface are a subset of the freedom names of the agent, and the other names are hidden. Then the process $AComp / (fn (AComp) - fn (p))$ is weak equivalent to P.

According to Definition 4, the interfaces can be obtained by name hiding. However, not every process satisfying Definition 4 correctly represents the internal implementations of an agent. The compatibility of the interfaces and implementations of an agent must be considered. The compatibility is defined as follows.

Definition 5

(Compatibility) Let EA be an agent and $P = {P_{1}, \dots, P_{n}}$ a set of its interfaces. The internal implementations of EA are compatible with interfaces P if

$fn (P_{i}) \cap fn (P_{j}) = \emptyset \forall i \neq j$ .

$EA \Rightarrow 0 iff \forall i, P_{i} \Rightarrow 0$ ( $\Rightarrow represents$ $(\overset{τ}{\to})^{*}$ , which shows 0 or some internal evolution sequence).

If $\exists α (α \neq τ), EA \overset{α}{\to} EA'$ , then $\exists i, P'_{i}, P_{i} \overset{α}{\to} P'_{i}$ and the internal implementations of $EA'$ are compatible with $P' = {P_{1}, \dots, P'_{i}, \dots, P_{n}}$ .

The compatibility between the interfaces and the internal implementations in an agent shows that the agent encapsulates its internal behaviors very well, so we can use the interfaces to represent the behaviors of the agent.³³

Analyzing consistency of RMSs

The agents automatically reconfigure to respond new requirements or to solve damages in RMSs. When new agents add or agents update, RMSs will evolve, and its consistency may be changed. The consistency means that all agents in RMSs successfully interact with each other, which is important for RMSs. As agents interact with each other via the interfaces, the consistency can be judged from the interface level.³³

If processes P and Q are consistent, P interacts with Q via an allelomorph name, such as $P = \bar{a} 〈 b 〉 . P', Q = a (c) . Q'$ . Then P and Q are synchronous.

Definition 6

(Consistency) Suppose the relation R in synchronous processes P and Q. If the replacer operator $σ \notin fn (P) \cup fn (Q)$ satisfies $P σ RQ σ$ , and

If $P \overset{τ}{\to} P'$ , then $P' RQ$ .

If $\neg (P ~ 0) \land \neg (P \equiv 0), P \overset{x (z)}{\to} P' \land Q \overset{\bar{x} y}{\to} Q'$ , then $P' {y / z} RQ'$ .

If $\neg (P ~ 0) \land \neg (P \equiv 0), P \overset{x (n)}{\to} P' \land Q \overset{\bar{x} (n)}{\to} Q'$ , then $P' RQ'$ .

Then R is called half-consistency. If R and $R^{- 1}$ are half-consistency, then R is consistency, denoted $as ~$ .

The consistency of the processes means that the processes can communicate with allelomorph names and execute successfully until their final states. If there exists a process $P'$ , $P'$ makes $P \Rightarrow P'$ and $P' \overset{τ}{\to}$ or $P' \equiv 0$ ( $P' \overset{τ}{\to}$ means $\exists P ″, P' \overset{τ}{\to} P ″$ ), then P can successfully execute until its final states. If $P \Rightarrow P', \neg (P' \overset{τ}{\to})$ and $\neg (P' \equiv 0)$ , then P is deadlock.

Theorem 1

(Consistency of agents) Suppose that P and Q are the interfaces of $ACom p_{1}$ and $ACom p_{2}$ , and P and Q are consistent, $P ~ Q$ . Then $ACom p_{1}$ and $ACom p_{2}$ are consistent, namely, $ACom p_{1} | ACom p_{2}$ can successfully execute.

Proof

We need to prove that if $P ~ Q$ , then $(ν fn (P) \cup fn (Q)) (P | Q)$ is successful. Namely, there exists a process S (Success), then $(ν fn (P) \cup fn (Q)) (P | Q) \Rightarrow S$ , in which $P \overset{τ}{\to}$ or $S \equiv 0$ . Suppose $fn (P) \cup fn (Q) = N$ , then $(ν fn (P) \cup fn (Q) (P | Q) = (ν N) (P | Q) \Rightarrow S$ . The proof is done by induction on the number n of τ-transitions leading to success.

Base case. Suppose $n = 0$ . As $P ~ Q$ , P and Q are the synchronous processes, then $\exists α$ , $P \overset{α}{\to}$ and $Q \overset{\bar{α}}{\to}$ , $α$ interacts with $\bar{α}$ using a shared allelomorph names, which is internal evolution in the process, so $(ν N) (P | Q) \overset{τ}{\to}$ holds.

Inductive hypothesis. Suppose $n = k, k > 0$ , $\forall P', Q'$ , $P' ~ Q'$ , $(ν N) (P' | Q') (\overset{τ}{\to})^{k} S$ holds, in which $S \overset{τ}{\to}$ or $S \equiv 0$ .

General case. Suppose $n = k + 1$ , $(ν N) (P | Q) \overset{τ}{\to} (ν N) (P' | Q') (\overset{τ}{\to})^{k} S$ holds. Then, the initial τ-transition is one of the following:

$P \overset{τ}{\to} P'$ . Since $P ~ Q$ , then $P' ~ Q$ .

$Q \overset{τ}{\to} Q'$ . Since $P ~ Q$ , then $P ~ Q'$ .

$P \overset{x (z)}{\to} P'$ , and $Q \overset{\bar{x} y}{\to} Q'$ . Since $P ~ Q$ , then $P' {y / z} ~ Q'$ .

$P \overset{x (n)}{\to} P'$ , and $Q \overset{\bar{x} (n)}{\to} Q'$ . Since $P ~ Q$ , then $P' ~ Q'$ .

$Q \overset{x (z)}{\to} Q'$ , and $P \overset{\bar{x} (y)}{\to} P'$ . Since $P ~ Q$ , then $P' ~ Q' {y / z}$ .

$Q \overset{x (n)}{\to} Q'$ , and $P \overset{\bar{x} (n)}{\to} P'$ . Since $P ~ Q$ , then $P' ~ Q'$ .

Consequently, if $(ν N) (P | Q) \overset{τ}{\to} (ν N) (P' | Q')$ , then $P' ~ Q'$ . Using the inductive hypothesis, we infer that $(ν fn (P) \cup fn (Q)) (P | Q)$ can successfully execute and then $ACom p_{1}$ and $ACom p_{2}$ satisfy consistency.

Theorem 1. ensures the matching of actions in the agents. For the agents with more interfaces, we can extend Theorem 1 to prove their consistency.

Theorem 2. (Consistency of RMSs) If all agents in RMSs can satisfy the consistency, then RMSs are consistent and can successfully execute.

We can prove Theorem 2 from Theorem 1, and the proof is omitted here.

Example 3

Consider the RMS in Example 2. To meet the market requirements, a drilling machine is added in the system. The drilling machine interacts with the robot, which can be described as follows

DrillingMachine (load, unload) = load (x) . Produce (x) .

DrillingMachine (load, unload) + \bar{unload} (p) .

DrillingMachine (load, unload)

From Definition 4, the interfaces of the drilling machine can be represented as manufacture and storage

\begin{matrix} Manufacture (load) = load (x) . Manufacture (load) \\ Storage (unload) = \bar{unload} (p) . Storage (unload) \end{matrix}

The interfaces of the robot interacting with the drilling machine are

\begin{matrix} RDLoad (load) = \bar{load} (item) . RDLoad (load) \\ RDUnload (unload) = unload (y) . RDUnload (unload) \end{matrix}

From Definition 6, we can get

\begin{matrix} Manufacture (load) ~ RDLoad (load) \\ Storage (unload) ~ RDUnload (unload) \end{matrix}

Hence, from Theorems 1 and 2, we have also that

DrillingMachine | Robot | LatheMachine |

MillingMachine | Buffer

is successful. Therefore, these machines, robot, and buffer can be safely composed to build a new RMS.

Conclusion

In order to respond to some new market requirements, improve the productivity, or deal with structural problems, reconfigurable manufacturing systems change their structures during the run-time. The development of RMSs is a very challenging issue. Formal methods are widely used to model, analyze, and verify RMSs. This work presents the RMS formal model based on OPNs and π-calculus, in which OPNs are employed to visualize initial structure as well as system behaviors of RMSs, while π-calculus is used to describe the reconfiguration of RMSs. Finally, the consistency of RMSs is analyzed using π-calculus.

Footnotes

Academic Editor: Jiacun Wang

Declaration of conflicting interests

The author(s) declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.

Funding

The author(s) disclosed receipt of the following financial support for the research, authorship, and/or publication of this article: This work was supported by the National Natural Science Foundation of China (grant nos 61202128, 71571190) and the National Aviation Science Foundation of China (grant no. 20125896020).

References

Zhou

ZW.

Resource-oriented Petri net for deadlock avoidance in flexible assembly systems. IEEE T Syst Man Cy A 2008; 38: 56–69.

Zhou

MC.

Elementary siphons of Petri nets and their application to deadlock prevention in flexible manufacturing systems. IEEE T Syst Man Cy A 2004; 34: 38–51.

Molina

Rodriguez

Ahuett

. Next-generation manufacturing systems: key research issues in developing and integrating reconfigurable and intelligent machines. Int J Comp Integ M 2005; 18: 525–536.

Dai

Meng

Hierarchical Petri net modelling of reconfigurable manufacturing systems with improved net rewriting systems. Int J Comp Integ M 2009; 22: 158–177.

Dai

Meng

. Rapid design and reconfiguration of Petri net models for reconfigurable manufacturing cells with improved net rewriting systems and activity diagrams. Comput Ind Eng 2009; 57: 1431–1451.

Cortes

Eles

Peng

Modeling and formal verification of embedded systems based on a Petri net representation. J Syst Architect 2003; 49: 571–598.

Lee

Sokolsky

Chen

. Challenges and research directions in medical cyber-physical systems. P IEEE 2012; 100: 75–90.

Chen

Barkaoui

. New Petri net structure and its application to optimal supervisory control: interval inhibitor arcs. IEEE T Syst Man Cy A 2014; 44: 1384–1400.

Wang

AR.

Design of liveness-enforcing supervisors for flexible manufacturing systems using Petri nets. IEEE T Syst Man Cy C 2007; 37: 517–526.

10.

Zhang

Khalgui

. Reconfigurable coordination of distributed discrete event control systems. IEEE T Contr Syst T 2015; 23: 323–330.

11.

Zhou

MC.

Control of elementary and dependent siphons in Petri nets and their application. IEEE T Syst Man Cy A 2008; 38: 133–148.

12.

Meng

Modeling of reconfigurable manufacturing systems based on colored timed object-oriented Petri nets. J Manuf Syst 2010; 29: 81–90.

13.

Zhou

MC.

Intelligent token Petri nets for modelling and control of reconfigurable automated manufacturing systems with dynamical changes. T I Meas Control 2009; 33: 9–29.

14.

De Silva

Benitez-Pina

Blos

. Modeling of reconfigurable distributed manufacturing control systems. IFAC: PapersOnLine 2015; 48: 1284–1289.

15.

Tarnauca

Puiu

Comnac

Modelling a flexible manufacturing system using reconfigurable finite capacity Petri nets. In: Proceedings of the 13th international conference on optimization of electrical and electronic equipment, Brasov, 24–26 May 2012, pp.1079–1084. New York: IEEE.

16.

Dai

Meng

Automatic reconfiguration of Petri net controllers for reconfigurable manufacturing systems with an improved net rewriting system-based approach. IEEE T Autom Sci Eng 2009; 6: 156–167.

17.

Kahloul

Bourekkache

Djouani

. Using high level Petri nets in the modelling, simulation and verification of reconfigurable manufacturing systems. Int J Softw Eng Know 2014; 24: 419–443.

18.

Zhao

On controllability of dependent siphons for deadlock prevention in generalized Petri nets. IEEE T Syst Man Cy A 2008; 38: 369–384.

19.

Giua

Decentralized supervision of Petri nets with a coordinator. IEEE T Syst Man Cy 2015; 45: 955–966.

20.

Giua

Design of optimal Petri net controllers for disjunctive generalized mutual exclusion constraints. IEEE T Automat Contr 2015; 60: 1774–1785.

21.

Zhou

ZW.

Short-term scheduling of crude-oil operations: enhancement of crude-oil operations scheduling using a Petri net-based control-theoretic approach. IEEE Robot Autom Mag 2015; 22: 64–76.

22.

Chen

Barkaoui

. On the enforcement of a class of nonlinear constraints on Petri nets. Automatica 2015; 55: 116–124.

23.

Bai

. Optimal one-wafer cyclic scheduling and buffer space configuration for single-arm multicluster tools with linear topology. IEEE T Syst Man Cy 2016; 46: 1456–1467.

24.

Best

Devillers

Koutny

Petri net algebra. Berlin: Springer, 2001.

25.

Miyamoto

Kumagai

A survey of object-oriented Petri nets and analysis methods. IEICE Trans Fundam 2005; E88-A: 2964–2971.

26.

Liu

. Modeling and analyzing software architecture using object-oriented Petri nets and π-calculus. Petri Nets Applications. Croatia: InTechOpen, 2010.

27.

ZH.

Approaches to formal modeling methodology for multi-agent systems. PhD Thesis, Xi’an Jiaotong University, Xi’an, China, 2006.

28.

Milner

Parrow

Walker

A calculus of mobile processes. J Inform Comput 1992; 100: 1–77.

29.

Milner

The polyadic π-calculus: a tutorial. Berlin: Springer-Verlag, 1993.

30.

Shen

Hao

Yoon

. Applications of agent-based systems in intelligent manufacturing: an updated review. Adv Eng Inform 2006; 20: 415–431.

31.

Wang

Khemaissia

Khalgui

. Dynamic low-power reconfiguration of real-time systems with periodic and probabilistic tasks. IEEE T Autom Sci Eng 2015; 12: 258–271.

32.

Jennings

Sycara

Wooldridge

MJ.

A roadmap of agent research and development. Auton Agent Multi-Ag 1998; 1: 7–38.

33.

Canal

Pimentel

Troya

JM.

Compatibility and inheritance in software architectures. Sci Comput Program 2001; 41: 105–138.