The Refinement of Petri Net with Inhibitor Arcs Based Representation for Embedded Systems

Abstract

Embedded systems are widely used in various devices. PRES+ (Petri net- based Representation for Embedded Systems) has been used to model and analyze embedded systems. However, it cannot characterize the priority of events, and cannot fully express the complex data flow and control flow. To solve this problem, inhibitor arcs are added to PRES+ and PIRES+ (PRES+ with Inhibitor arcs) is obtained. However, PIRES+’s state space explosion problem is a handicap when modeling, verifying, and controlling complex, large embedded systems. To mitigate the state space explosion problem of PIRES+ and analyze complex embedded systems, we propose the place refinement approach and the place set refinement approach for PIRES+. Under specific conditions, several important properties of PIRES+, such as timing, functionality, reachability, liveness, and boundedness, are preserved by using these refinement approaches. In order to illustrate the effectiveness of these refinement methods, as an example, the modeling and analysis of a network communication system is proposed. The refinement methods proposed have certain feasibility and practicability and provide a more practical theoretical basis for the modeling of some embedded systems.

1. Introduction

Embedded systems are used in diverse contexts from automobiles to communication systems, home appliances, and the Internet of Things, and are becoming more and more complex with increasing requirements. Therefore, higher requirements are put forward for the reliability, correctness, and timing of the embedded system, so it is important to focus on both how to model embedded systems and how to guarantee their correctness.

In the literature, there exist many models to represent embedded systems [1,2], such as finite state machines [3], data flow graphs [4], Petri nets [5], and communicating processes [6], etc. These formal modeling methods describe the characteristics of embedded systems from different aspects, but do not form a unified standard. Petri net has a formal mathematical definition and standardized derivation rules, which is a more standardized formal modeling method.

Ordinary Petri nets can describe systems with features such as concurrency, conflict, and uncertainty. However, there are several drawbacks when it comes to modeling embedded systems: ordinary Petri nets have no hierarchical structure, lack the notion of time, and have a limited ability to describe data flows. In order to overcome these drawbacks, several extended Petri nets for an embedded system’s modeling have been proposed, such as colored Petri net [7], logical delay Petri net, time Petri net [8], hybrid Petri net, fuzzy Petri net, PRES+ (Petri net-based Representation for Embedded Systems) [9], etc. These extended forms of Petri nets start from different application requirements and improve the ability to model and analyze embedded systems.

Among them, PRES+ is an extended Petri net, and has previously been presented to represent embedded systems. Based on PRES+, Cortés et al. [9] proposed a computation model for embedded systems and gave a method to solve the formal verification problem of the PRES+ model. Karlsson et al. [10] proposed a verification approach for the PRES+ by using a divide-and-conquer approach. In order to enhance the verification effectiveness of PRES+, Xia [11] presented transition refinement method. A sharing synthesis approach for PRES+ is presented in [12]. Under certain constraints, the synthesis PRES+ will preserve boundedness and liveness. A more formal successor marking definition of PRES+ is proposed in [13]. In order to analyze complex embedded systems, Xia et al. [14] proposed two kinds of transition synthesis methods for PRES+.

Although PRES+ can represent the embedded system at different levels, capture the real-time information of the embedded system, and describe the uncertainty of the system, the PRES+ model cannot describe the priority of events, and cannot fully express the complex data flow and control flow.

Adding inhibitor arcs to Petri nets can improve the analysis ability of Petri nets [15]. The Petri net with inhibitor arcs not only has the ability of zero detection, but also can simulate any random access machine. Inhibitor arcs can be used to control the sequence of transitions and describe the priority relationship between events. In embedded systems, some transitions occur successively under certain conditions, which affect the expression of data flow and control flow. Therefore, it is necessary to introduce inhibitor arcs. In order to improve the modeling and analysis ability of PRES+, we add inhibitor arcs into PRES+, and obtain PIRES+ (Petri net with Inhibitor arcs-based Representation for Embedded Systems).

However, when large complex embedded systems are modeled by PIRES+, the state space explosion problem is a major disadvantage for PIRES+. In the literature, many authors have investigated Petri net transformation methods to mitigate the problem of state space explosion. The three popular transformations of Petri net are refinement [11,16,17,18,19,20,21,22,23,24,25,26,27,28,29], reduction [30,31,32,33], and synthesis [12,14,34,35,36,37,38,39].

Petri net-based refinement is an important method to system design and verification. As for refinement, Huang et al. [16] presented several refinement conditions to preserve 19 properties for Place/Transition Petri nets. Padberg et al. [17] provided a thorough survey of refinements based on several nets, namely place/transition nets, predicate/transition nets, and elementary nets. For colored Petri nets (CPNs), Lakos et al. [18] gave three types of refinement: node refinement, type refinement, and subnet refinement. Mejía et al. [19] presented a refinement process for extended attribute time place Petri nets. For workflow nets, Hee et al. [20] proposed several refinement rules which preserve soundness under certain conditions. Li et al. [21] defined algebraic steps for refinement and reduction, and investigated the Petri net property preservation. Xia [22] proposed a place type refinement method for ordinary Petri nets. Under certain conditions, liveness, boundedness, and reversibility of these refined nets are preserved.

A top-down methodology achieves a formal specification of the logic control structure, refines the model so that more system operation details can be included, and consequently implements the control at a physical level [23]. Choppy et al. [24] investigated a refinement method of colored Petri net subclass and proved the correctness of this method. For a kind of well-behaved Petri net, Ding et al. [25] proposed a refinement approach. Wang et al. [26] proposed a refinement approach which may not require reachability analysis. For systems specified in Elementary Net Systems, Bernardinello et al. [27] presented a refinement method for distributed systems. Lacheheub et al. [28] focused on analyzing the transformation of the business process (BP) to the Petri net and gave the transition refinement operation to verify soundness, liveness, and boundedness. Based on the UML state machine and the Petri net model, Łabiak et al. [29] presented a design of digital controllers. Petri nets were applied for macroplaces’ hierarchy and some elements of modularity.

Cortés et al. [9] extended PRES+ by introducing the definition of hierarchy and proposed some concepts of equivalence for the PRES+ model. A strong refinement and a wake refinement of a certain transition were presented. These refinements preserve equivalence. In [11], we extended the concepts of refinement in [9] and investigated transition refinement approaches for PRES+.

In order to model, analyze, and verify large complex embedded systems, and to resolve PIRES+’s state space explosion problem, the main contributions of this work include: (1) refinement methods for PIRES+ are proposed; (2) the property preservation of the refinement methods is investigated.

Compared with several refinement methods for ordinary Petri nets [16,22], Colored Petri nets [18], and PRES+ [9,11], the refinement methods for PIRES+ can nicely describe the characteristics of embedded systems.

Specifically, we first give the refinement approaches for PIRES+, and then investigate their property preservations. Under some constraints, reachability, timing, functionality, liveness, and boundedness of PIRES+ are preserved. Since these refinement methods can preserve these important properties, there is no need for using reachability analysis when the PIRES+ model is expanded. Thus, these refinement approaches can mitigate PRES+’s state space explosion problem.

The rest of the paper is structured as follows. Basic notions of PIRES+ are presented in Section 2. Section 3 proposes the refinement methods of PIRES+. Section 4 investigates reachability, functionality, and timing preservation. Section 5 studies the preservation of boundedness and liveness of PIRES+. Section 6 illustrates the efficiency of the PIRES+ refinement methods with an applicable example. We conclude by summarizing the contributions of the refinement technique in Section 7.

2. Basic Notions of PIRES+

In the following, we add inhibitor arcs into PRES+, and obtain PIRES+. The PIRES+ model can capture an embedded system’s timing aspects and obtain both control and data information which fully express complex data flow and control flow.

Definition 1.

A Petri net with inhibitor arcs is a five-tuple$N=\left(P,T,F,I,M\right)$, where$\left(P,T,F\right)$represents a net,$M_0$is the initial marking,$I\subset P\times T$is a set of inhibitor arcs,$I\cap F=\varnothing$.

Figure 1 shows an example of the Petri net with inhibitor arcs. For example, there are inhibition arcs $I=\left\{\left(p_3,t_1\right),\left(p_6,t_2\right)\right\}$ in Figure 1. The initial marking is [1,0,1,0,0,0]^T. At the initial marking $M_0$, for transitions $t_1$ and $t_2$, $\forall pϵt_i:M\left(p\right)\ge 1,i\in \left\{1,2\right\}$. Since $M_0\left(p_3\right)=1$ and $\left(p_3,t_1\right)\in I$, $t_1$ is not an enabled transition. At the same time, $\left(p_6,t_2\right)\in I$, and $M_0\left(p_6\right)=0$, $t_2$ is an enabled transition.

Definition 2.

Ref. [9] A PRES+ model is $N=\left(P,T,I,O,M_0\right)$, where $P=\{p_1$, $p_2$, ……, $p_m\}$ is a finite non-empty set of places, $T=\{t_1$, $t_2$,……, $t_n\}$ is a finite non-empty set of transitions, $I\subseteq P\times T$ is a finite non-empty set of input arcs, $O\subseteq T\times P$ is a finite non-empty set of output arcs, and $M_0$ is the initial marking, $k=〈v,r〉$ is a token, where $v$ is the token value, and $r$ is the token time.

The inhibitor arcs are added to the PRES+, the PIRES+ (PRES+ with inhibitor arcs) is obtained.

Definition 3.

$N=\left(P,T,F_I,F_O,I,M_0\right)$is a PIRES+ model, where$P=\{p_1$,$p_2$, ……,$p_m\}$is a finite non-empty set of places,$T=\{t_1$,$t_2$,……,$t_n\}$is a finite non-empty set of transitions,$F_I\subseteq P\times T$is a finite non-empty set of input arcs,$F_O\subseteq T\times P$is a finite non-empty set of output arcs,$I\subset P\times T$is a set of inhibitor arcs, and$M_0$is the initial marking.

Figure 2 gives an example of a PIRES+ model, where $P=\left\{p_0,p_1,p_2,p_3,p_4,p_5\right\}$, $T=\left\{t_0,t_1,t_2,t_3,t_4\right\}$, $F_I=\left\{\left(p_0,t_0\right),\left(p_1,t_1\right),\left(p_1,t_4\right),\left(p_2,t_2\right),\left(p_3,t_2\right),\left(p_4,t_3\right),\left(p_5,t_2\right)\right\}$, $F_O=\{(t_0,p_1$), $\left(t_0,p_2\right)$, ($t_1$, $p_3),$ ($t_2,p_4),\left(t_3,p_0\right),\left(t_4,p_3\right)\}$, $\mathrm{and} I=\left\{\left(p_5,t_4\right)\right\}$.

Definition 4.

A token in PIRES+ is$k=〈v,r〉$, where$v$is the token value, and$r$is the token time, which is a nonnegative real number describing the time stamp of the token.

In Figure 2, for instance, the token of place $p_0$ is $k_0=〈3,0〉$, where the token value is 3 and the time stamp is 0.

Definition 5.

For every transition$t\in T$, there is transition function $f:\tau \left(p_1\right)\times \tau \left(p_2\right)\times \dots \dots \times \tau \left(p_a\right)\to \tau \left(q\right)$, where $\tau$ is a type function, $•t=\left\{p_1,p_2,\dots \dots ,p_a\right\}$, $q\in t•.$

For instance, in Figure 2, $t_1$ has the function $f_1=v_1+3$, where $v_1$ is the value of the token that will appear in $p_1$, and after $t_1$ fires, the value of the token in $p_3$ will be the value of the token in $p_1$ plus 3.

Definition 6.

For every transition$t\in T$, there are$d^{-},d^{+}\in R^{+}$, where$d^{-}$is a minimum delay,$d^{+}$is a maximum delay, and$R^{+}$is the non-negative real number set.

For instance, in Figure 2, the delay of $t_3$ is [2,5].

Definition 7.

A transition$t\in T$may have a guard$G$:$\tau \left(p_1\right)\times \tau \left(p_2\right)\times \dots \dots \times \tau \left(p_a\right)\to \left\{0,1\right\}$, where$•t=\left\{p_1,p_2,\dots \dots ,p_a\right\}.$

The guard is an important factor to determine whether $t$ can be enabled. In Figure 2, transition $t_2$ has guard $G=TURE$ if $v_3>v_2$, where $v_2$ and $v_3$ are the values of the tokens in places $p_2$ and $p_3$, respectively.

Definition 8.

$b=\left(k_1,k_2,\dots \dots ,k_a\right)$is a binding of transition$t$, where$\forall p_i\in •t,k_i\in M\left(p_i\right)$.

Definition 9.

Ref. [9] For an enabled transition $t$, there exists the enabling time $et$, where $et$ is the time instant at which $t$ becomes enabled and is given by the maximum token time of the tokens in the binding.

Definition 10.

For an enabled transition$t$, there exists the earliest trigger time$t^{-}=et+d^{-}$and the latest trigger time$t^{+}=et+d^{+}$.

As in P/T Petri nets, when a transition is enabled in the PIRES+ model, it can be fired.

Definition 11.

The firing of transition$t$for a binding$b$changes$M$into a new marking$M\prime$:

(i) 

Tokens from$•t$are removed, i.e.,$\forall p_i\in •t,M\prime \left(p_i\right)=M\left(p_i\right)-\left\{k_i\right\}$.

(ii) 

A new token $k=〈v,r〉$is put into each place of$t•$, i.e., $M\prime \left(p\right)=M\left(p\right)+\left\{k\right\}$for every $p\in •t$.

(iii) 

The marking of places different from •$t$ and $t$ • remain unchanged, i.e., $\forall p\in P-\left\{•t \cup t•\right\},M\prime \left(p\right)=M\left(p\right)$.

3. Refinement Operations for PIRES+

In this section, we will investigate the refinement operation for the PIRES+ model. First, several relevant concepts will be proposed. Then, we propose the refinement operations.

Definition 12.

Suppose$N=\left(P,T,F_I,F_O,I,M_0\right)$is a PIRES+ model.$N_p=(P_p,T_p,F_{Ip},F_{Op},I_p, M_{p,0}$) is called a place subnet of$N$if and only if:

(i) 

$P_p\subset P,T_p\subset T$and$P_p\ne \varnothing ,T_p\ne \varnothing$;

(ii) 

$F_{Ip}=F_I\cap \left(P_p\times T_p\right)$and$F_{Op}=F_O\cap \left(T_p\times P_p\right)$;

(iii) 

$•T_p\cup T_p•\subseteq P_p$;

(iv) 

$I_p\subseteq I$;

(v) 

$N_p$is connected,$\left\{p_{in},p_{out}\right\}\subseteq P_p$, where$p_{in}$is the only input place of$N_p$,$p_{out}$is the only output place of$N_p$;

(vi) 

$\forall t\in T_P$,$\exists f:\tau \left(p_1\right)\times \tau \left(p_2\right)\times \dots \dots \times \tau \left(p_a\right)\to \tau \left(q\right)$(where$q\in t•$,$•t=\{p_1,\dots \dots ,p_a$});

(vii) 

$\forall t\in T_P$,$\exists d^{-},d^{+}\in R^{+}$, where$d^{-}$is a minimum delay,$d^{+}$is a maximum delay,$R^{+}$is the set of non-negative real numbers, and$d^{-}\le d^{+}$.

Definition 13

For the transition set$T_p$of$N_p$, there is a minimum delay$d_p^{-}$and a maximum delay$d_p^{+}$, i.e.,$\exists d_p^{-},d_p^{+}\in R^{+}$such that$d_p^{-}\le d_p^{+}$.

Definition 14. 

For the transition set$T_p$of$N_p$, there exists a transition set function$f_p$, i.e.,$\exists f_p:\tau \left(p_1\right)\times \tau \left(p_2\right)\times \dots \dots \times \tau \left(p_a\right)\to \tau \left(q\right)$, where$•T_p=\left\{p_1,p_2,\dots \dots ,p_n\right\}$and$q\in T_p•$.

In order to investigate property preservations in Section 4 and Section 5, we propose the following supposition for the PIRES+ subnet.

Supposition 1.

Suppose that PIRES+ subnet$N_p=\left(P_p,T_p,F_{Ip},F_{Op},I_p,M_{p,0}\right)$satisfies:

(i) 

In a process, i.e., tokens flow from outside of$N_p$into$p_{in}$, through$N_p$, then flow out from$p_{out}$, the tokens’ number flowing into$p_{in}$is equal to that flowing out from$p_{out}$.

(ii) 

$p_{in}$is the unique place of$P_p$which may contain tokens.

In this subsection, we present the PIRES+ refinement operations.

Definition 15. 

PIRES+ refinement operation Re$f_p\left(p_p,N_p\right)$: let the refined PIRES+ $N^{\prime }=$ $(P^{\prime },T\prime ,F_I\prime ,F_O\prime ,I\prime ,M_0\prime )$ be obtained from $N=\left(P,T,F_I,F_O,I,M_0\right)$ using $N_p=(P_p,T_p,F_{Ip}$, $F_{Op},I_p{M}_{p,0})$ to replace $p_p$ where,

(i) 

$P^{\prime }=P_p\cup P-\left\{p_p\right\}$;$T^{\prime }=T_p\cup T$;$I^{\prime }=I\cup I_p$;

(ii) 

If$\left(p,t\right)\in F_{Ip}\cup F_I$, then$\left(p,t\right)\in F_I\prime$; If$\left(t,p\right)\in F_{Op}\cup F_O$, then$\left(t,p\right)\in F_O\prime$;

(iii) 

If$\left(t,p_p\right)\in F_O$, then$\left(t,p_{in}\right)\in F_O\prime$; If$\left(p_p,t\right)\in F_I$, then$\left(p_{out},t\right)\in F_I\prime$;

(iv) 

$M_0\prime =\left\{\begin{array}{c}\left(M_{\left(P-\left\{p_p\right\}\right)0}, {\theta }_p\right) M_0\left(p_p\right)=0\\ \left(M_{\left(P-\left\{p_p\right\}\right)}, {\theta }_{p0}\right) M_0\left(p_p\right)>0\end{array}\right.$(where$M_{\left(P-\left\{p_p\right\}\right)}$is the projection of$M$on$P-\left\{ p_p\right\}$, and${\theta }_p$is 0-vector of$M_p$);

(v) 

$f_p\circ f_{•p_{in}}=f_{•p_p},f_{out•}=f_{p_p•}$;

(vi) 

$d_{•p_{in}}^{-}+d_p^{-}=d_{•p_p}^{-}$,$d_{•p_{in}}^{+}+d_p^{+}=d_{•p_p}^{+}$;$d_{p_{out•}}^{-}=d_{p_{p•}}^{-}$,$d_{p_{out•}}^{+}=d_{p_p•}^{+}$.

Note that, although in Definition 15, only $p_p$ of $N$ is replaced by a subnet $N_p$, this refinement operation can be extended to the place set refinement operation. Let the place set $P_{set}$ have a finite number of places. Every place of $P_{set}$ may not be in conflict with other places of $P_{set}$, i.e., $\forall p_1,p_2\in P_{set}$, $•p_1\cap •p_2$ = $\varnothing$ and $p_1•\cap p_2•$ = $\varnothing$ (where $p_1\ne p_2$). In other words, every place of $P_{set}$ may not share output transitions and input transitions with other places of $P_{set}$.

Supposition 2. 

Suppose (i)$P_{set}=\left\{p_1,p_2,\dots \dots ,p_m\right\}\left(m\ge 2\right)$is a place set of$N$, with$•p_i\cap •p_j$=$\varnothing$and$p_i•\cap p_j•$=$\varnothing$for$\forall p_i,p_j\in P_{set}$(where$i\ne j$); (ii)$N_{set}=\left(N_{p1},N_{p2},\dots \dots ,N_{pm}\right)$, where$N_{pi}\left(i=1,2,\dots \dots ,m\right)$is the subnet of$N$.

Definition 16. 

PIRES+ place set refinement operation Re$f_{p_{set}}\left(P_{set},N_{set}\right)$: let the refined PIRES+$N\prime =\left(P\prime ,T\prime ,F_I\prime ,F_O\prime ,I\prime ,M_0\prime \right)$be obtained from$N=\left(P,T,F_I,F_O,I,M_0\right)$using place subnets$N_{p1},N_{p2},\dots \dots ,N_{pm}$to replace$p_1,p_2,\dots \dots ,p_m$of$P_{set}$, respectively.

Note that, since every place of $P_{set}$ may not share output transitions and input transitions with other places of $P_{set}$, the specific execution process of this place set operation is as follows. First, let $N_1=\left(P_1,T_1,F_{I1},F_{O1},I_1,M_{1,0}\right)$ be obtained from $N=(P,T,F_I,F_O,I,M_0$) using $N_{p1}$ to replace $p_1$ of $N$; second, let $N_2=\left(P_2,T_2,F_{I2},F_{O2},I_2,M_{2,0}\right)$ be obtained from $N_1=\left(P_1,T_1,F_{I1},F_{O1},I_1,M_{1,0}\right)$ using $N_{p2}$ to replace $p_2$ of $N_1$; …; last, let $N\prime =\left(P\prime ,T\prime ,F_I\prime ,F_O\prime ,I\prime ,M_0\prime \right)$ be obtained from $N_{m-1}=\left(P_{m-1},T_{m-1},F_{I,m-1},F_{O,m-1},I_{m-1},M_{m-1,0}\right)$ using $N_{pm}$ to replace $p_m$ of $N_{m-1}$.

4. Preservation of Reachability, Timing, and Functionality for PIRES+

In this section, we investigate the preservation of reachability, functionality, and timing of the refined PIRES+ model by using the refinement operations. First, we propose the concepts of the property preservations of PIRES+. Second, we study the reachability, timing, and functionality preservations of PIRES+.

Definition 17. 

PIRES+ subnets$N_{p1}$and$N_{p2}$are said to have the same reachability iff:

(i) 

The input place’s number and the output place’s number of$N_{p1}$are the same as those of$N_{p2}$;

(ii) 

The tokens’ number within the input places of$N_{p1}$is equal to that of$N_{p2}$, and when these tokens go through $N_{p1}$and$N_{p2}$, respectively, the number of tokens of $N_{p1}$is the same as that of$N_{p2}$.

Definition 18. 

PIRES+ subnets$N_{p1}$and$N_{p2}$are said to have the same functionality iff:

(i) 

The reachability of$N_{p1}$is the same as that of$N_{p2}$;

(ii) 

If when the token type of tokens in the input places of $N_{p1}$is equal to that of$N_{p2}$, then the token type of tokens in the output places of$N_{p1}$is equal to that of$N_{p2}$.

Definition 19. 

PIRES+ subnets$N_{p1}$and$N_{p2}$are said to have the same timing iff:

(i) 

The reachability of$N_{p1}$is the same as that of$N_{p2}$;

(ii) 

The token time of tokens in the input places of$N_{p1}$is equal to that of$N_{p2}$, and the token time of tokens in the output places of$N_{p1}$is equal to that of$N_{p2}$.

In the following, reachability, functionality, and timing preservations of these refinement operations will be investigated.

Theorem 1. 

Let PIRES+$N\prime =\left(P\prime ,T\prime ,F_I\prime ,F_O\prime ,I\prime ,M_0\prime \right)$be obtained from$N=\left(P,T,F_I,F_O,I,M_0\right)$using PIRES+ refinement operation Re$f_p\left(p_p,N_{pp}\right)$. Then,$N\prime$and$N$have the same reachability, functionality, and timing.

Proof. 

Suppose subnet $N_1=\left(P_1,T_1,F_{I1},F_{O1},I_1,M_{1,0}\right)$, where $P_1=\{•$($•p_p$), $p_p,\left(p_p•\right)•\}$, $T_1=\left\{•p_p\right\}\cup \left\{p_p•\right\}$, $F_{I1}=\left\{\left(p_p,t\right)|t\in p_p•\right\}\cup \left\{\left(p,t\right)|p\in •\left(•p_p\right)\wedge t\in •p_p\right\}$, $F_{O1}=\left\{\left(t,p\right)\right|t\in p_p•\wedge \mathrm{p}\in \left(p_p•\right)•\cup \left\{\left(t,p_p\right)\right|t\in •p_p\}$, $I_1=\varnothing$, $M_{p_{p,}0}=M_0|P_{p_p}$.

Suppose subnet $N_2=\left(P_2,T_2,F_{I2},F_{O2},I_2,M_{2,0}\right)$ where $P_2=\left\{•\left(•p_p\right),\left(p_p•\right)•\right\}\cup P_{pp}$, $T_2=\left\{\left(•p_p\right),\left(p_p•\right)\cup T_{pp}\right\}$, $F_{I2}=F_{Ipp}\cup \left\{\left(p,t\right)\mathrm{t}\in •p_p\wedge p\in •\left(•p_p\right)\cup \left\{\left(p_{out},t\right)\mathrm{t}\in p_p•\right\}\right\}$, $F_{O2}=F_{Opp}\cup \{\left(t,p_{in}\right)\mathrm{t}\in •p_p\cup \{t,p)\mathrm{p}\in \left(p_p•\right)•\wedge \mathrm{t}\in p_p•\}\}$, $I_2=I_{pp}\cup I_1$. If $p\in P_{pp}$, then $M_{2,0}\left(p\right)=M_{pp,0}\left(p\right)$. If $p\in \left\{•\left(•p_p\right),\left(p_p•\right)•\right\}$, then $M_{2,0}\left(p\right)=M_{pp,0}\left(\left\{\left(p_p•\right)•\cup •\left(•p_p\right)\right\}\right)\left(p\right)$. □

We can see that $N_1$ and $N_2$ have the same input places and output places. According to Definition 15, the number of tokens in input places of $N_1$ is the same as that of $N_2$. Since PIRES+$N\prime$ is obtained from $N$ by using $N_2$ to replace $p_p$, by Supposition 1, Definitions 12, 15, the number of tokens in output places of $N_1$ is the same as that of $N_2$. By Definition 17, $N\prime$ and $N$ have the same reachability.

According to Definition 15, the type of tokens in input places of $N_1$ is the same as that of $N_2$. Since $f_{pp}\circ f_{•p_{in}}=f_{•p_p}$, $f_{p_{out•}}=f_{p_{p•}}$, then the type of tokens in output places of $N_1$ is the same as that of $N_2$. By Definition 18, $N\prime$ and $N$ have the same functionality.

By Definition 15, the time of tokens in input places of $N_1$ is the same as that of $N_2$. Since $d_{•p_{in}}^{-}+d_{p_p}^{-}=d_{•p_p}^{-}$, $d_{•p_{in}}^{+}+d_{p_p}^{+}=d_{•p_p}^{+}$, $d_{p_{out•}}^{-}=d_{p_p•}^{-}$ and $d_{p_{out•}}^{+}=d_{p_p•}^{+}$, by Definition 15, the time of tokens in output places of $N_1$ is the same as that of $N_2$. By Definition 19, $N\prime$ and $N$ have the same timing.

Since $N^{\prime }-N_2=N-N_1$, then $N\prime$ and $N$ have the same reachability, functionality, and timing. □

Note that, by Supposition 2, Definitions 15, 16, and Theorem 1, we can analyze the reachability, timing, and functionality preservations of the place set refinement operation.

Theorem 2. 

Suppose$P_p=\left\{p_1,p_2,\dots \dots ,p_m\right\}$($m\ge 2$) is the place set of PRES+$N$, and$\forall p_i,p_j\in P_p$(where$i\ne j$),$•p_i\cap •p_j$=$\varnothing$and$p_i•\cap p_j•$=$\varnothing$. Let$N\prime =\left(P\prime ,T\prime ,F_I\prime ,F_O\prime ,I\prime ,M_0\prime \right)$be obtained from$N=\left(P,T,F_I,F_O,I,M_0\right)$using place set refinement operation Re$f_{P_p}\left(P_p,N_p\right)$. Then,$N\prime$and$N$have the same reachability, functionality, and timing.

Proof. 

Since $P_p=\left\{p_1,p_2,\dots \dots ,p_m\right\}$ ($m\ge 2$) is the place set of $N$, and $\forall p_i,p_j\in P_p$ (where $i\ne j$), $•p_i\cap •p_j$ = $\varnothing$ and $p_i•\cap p_j•$ = $\varnothing$, we can refine these places one by one. First, let $N_1=\left(P_1,T_1,F_{I1},F_{O1},I_1,M_{1,0}\right)$ be obtained from $N=\left(P,T,F_I,F_O,I,M_0\right)$ using $N_{pp1}$ to replace $p_1$ of $N$, by the proof process of Theorem 1, $N_1$ and $N$ have the same reachability, functionality, and timing. Second, let $N_2=\left(P_2,T_2,F_{I2},F_{O2},I_2,M_{2,0}\right)$ be obtained from $N_1=\left(P_1,T_1,F_{I1},F_{O1},I_1,M_{1,0}\right)$ using $N_{pp2}$ to replace $p_2$ of $N_2$, by the proof process of Theorem 1, $N_2$ and $N_1$ have the same reachability, functionality, and timing. In the case of $p_3,\dots \dots ,p_m$, we can prove it in the same way. Thus, $N\prime$ and $N$ have the same reachability, functionality, and timing. □

5. Preservation of Liveness and Boundedness for PIRES+

In Petri net system, liveness and boundedness are the two important behavior properties. The liveness reflects that the net system can complete any part of work in any state. This means that there is no local deadlock in the Petri net system. The boundedness reflects the overflow resistance of the Petri net system.

Some studies have been conducted in the field of Petri net refinement aiming to realize the preservation of liveness and boundness [11,16,17,22]. Huang et al. [16] proposed several refinement approaches for Place/Transition Petri nets to preserve liveness and boundedness. Xia [22] presented a refinement operation for ordinary Petri nets and investigated the preservation of reversibility, boundedness, and liveness of the refined nets. In [11], we analyzed a kind of transition refinement method for PRES+ to preserve liveness and boundedness.

In this section, we investigate the refinement method of PIRES+, and propose certain constraints to preserve liveness and boundedness of PIRES+.

To explore the preservation of liveness and boundedness of the refinement approaches, the concepts of the state, liveness, and boundedness of PIRES+ should be presented.

Definition 20. 

$S=\left(M_v,J\right)$is said to be a state of PIRES+ model$N=\left(P,T,F_I,F_O,I,M_0\right)$, where$M_v\in R\left(M_0\right)$(where$R\left(M_0\right)$is the marking reachable set), and$J:T\to R^{+}\cup \left\{\#\right\}$(where$\#$denotes the unusable status).

Definition 21. 

$S_0=\left(M_0,J_0\right)$with$J_0\left(t\right)=\left\{\begin{array}{c}0 M_0 \left(p\right)\ge W\left(p,t\right) \forall p\in •t\\ \#, otherwise\end{array}\right.$(where$W\left(p,t\right)$denotes the weight function on$\left(p,t\right)$) is called the initial state of$N$.

Definition 22. 

Let$Z=\left(P,T,F_I,F_O,I\right)$be the skeleton of$N=\left(P,T,F_I,F_O,I,M_0\right)$. $\Sigma =\left(Z,S_0\right)$(where$S_0=\left(M_0,J_0\right)$) is called the PIRES+ net system of$N=\left(P,T,F_I,F_O,I,M_0\right)$.

Definition 23. 

Let$S$be a reachable state, and$t\in T$. If$\forall S\prime \in R_N\left(S\right),\exists S\prime \prime \in R_N\left(S\prime \right)$, such that$S\prime \prime \stackrel{t}{\to }$, then$t$is said to be live. If$\forall t$,$t$is live, then$\Sigma =\left(Z,S_0\right)$is said to be live.

Definition 24. 

If$S\in R_N$($S_0$),$\exists K>0$(where$K$is a natural number) such that$M\left(p\right)\le K$, then$p$is called bounded. For$\forall p$, if$p$is bounded, then the PIRES+ net system$\Sigma =\left(Z,S_0\right)$is said to be bounded.

In order to investigate liveness and boundedness preservations of the refinement operations, the concept of the PIRES+ place-closed net system should be proposed.

Definition 25. 

$\overline{\Sigma }$= ($\overline{Z_p}$,$\overline{S_{p0}}$) is called a place-closed PIRES+ net system if we add a transition$t_p$(where its transition delay is$\left[d_{t_p}^{-},d_{t_p}^{+}\right]$, and the transition function is$f_{t_p}$) and arcs$\left\{\left(p,t_p\right)|p\in \left(p_p•\right)•\right\}, \left\{\left(t_p,p\right)\right|p\in •\left(•p_p\right)\}$, to$\left(Z_p,S_{p0}\right)$and the marking of$\left(Z_p,S_{p0}\right)$is preserved.

In the following, the preservation of liveness and boundedness for PIRES+ will be studied.

Theorem 3. 

Suppose PIRES+ net system $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is obtained from $\Sigma =\left(Z,S_0\right)$ by the refinement operation Re $f_p\left(p_p,N_p\right)$. If $•\left(•p_{pin}\right)\in \left\{p\left|M_0^{\prime }\left(p\right)\right.〉0\wedge p\in P\prime \right\}$, then $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is live iff $\Sigma =\left(Z,S_0\right)$ and $\overline{\Sigma }$ = ($\overline{Z_p}$, $\overline{S_{p,0}}$) are live.

Proof. 

(If) $\forall t^{\prime }\in T^{\prime },$ there exists $t\prime \in T$ or $t\prime \in T_p$ in $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$. According to Supposition 1, for $\forall S\prime \in R\left(M_0\prime \right)$ (where $S\prime =\left[M_{\left(P-\left\{p_p\right\}\right)},M_p\right]$), there exists $M\in R\left(M_0\right)$ and $M_p\in R\left(M_{p,0}\right)$. If $t\prime \in T$, according to Definition 23, $\exists \overline{M}\in R\left(M\right)$, $\overline{S}\stackrel{t^{\prime }}{\to }$ for $M\in R\left(M_0\right)$. According to Definition 23, Definition 15, and Supposition 1, $\exists \overline{S_0}\prime =\left(\left(M_{\left(P-\left\{p_p\right\}\right)},M_p\right),J_0\prime \right)\in R\left(M\prime \right)$, such that $\overline{S}\stackrel{t^{\prime }}{\to }$ (where $\overline{M}\in R\left(M\right),\overline{M_p}\in R\left(M_p\right)$). So, in $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$, $t\prime$ is live. If $t\prime \in T_p$, according to Definition 23, $\exists \overline{M_p}\in R\left(M_p\right)$, such that $\overline{S_p}\stackrel{t^{\prime }}{\to }$. According to Definition 23, Definition 15, and Supposition 1, $\exists \overline{S_0}\prime \prime =\left(\left(M{\prime }_{\left(P-\left\{p_p\right\}\right)},M_p\right),J_0\prime \right)\in R\left(M\prime \right)$, such that $\overline{S}\prime \prime \stackrel{t^{\prime }}{\to }$. Then, $t\prime$ is live in $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$.

(Only-if) Let $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ be live. Suppose that $\Sigma =\left(Z,S_0\right)$ is not live, that is, $\exists S\in R\left(S_0\right),\exists t\in T$, $\forall \overline{S}\in R\left(S\right)$, such that $\neg \left(\overline{S}\stackrel{t}{\to }\right)$. Suppose $S_{\left\{P-p_p\right\},0}\stackrel{\sigma ,\tau }{\to }S\stackrel{\overline{\sigma },\overline{\tau }}{\to }\overline{S}$, where $\overline{\sigma },\sigma \in T$, and $S_{\left\{P-p_p\right\},0}$ is the projection of $S\prime \prime$ on $P-\left\{p_p\right\}$. Next, we add corresponding transition step ${\sigma }_p$ of ${\Sigma }_p=\left(Z_p,S_{p,0}\right)$ and obtain $\sigma \prime ,{\sigma }^{*}\in T^{″}$, $S_{\left\{P-p_p\right\},0}\stackrel{\sigma ,\tau }{\to }{S}_{\left\{P-p_p\right\}}\stackrel{\overline{\sigma },\overline{\tau }}{\to }{S}_{\left\{P-p_p\right\}}$. According to Definition 23, Definition 15, and Supposition 1, $S_0\prime \stackrel{{\sigma }^{\prime },{\tau }^{\prime }}{\to }S\prime \prime \stackrel{{\sigma }^{″},{\tau }^{″}}{\to }\overline{S}\prime \prime$, the projection of $S\prime \prime$ on $\overline{\Sigma }$ is $\overline{S}$, then $\exists t\prime \in T\prime ,S\prime \prime \in R\left(S_0\prime \prime \right)$, $\forall \overline{S}\prime \prime \in R\left(S\prime \right)$, such that $\neg (\overline{S}\stackrel{t^{\prime }}{\to })$$\to \neg (\overline{S}\prime \prime \stackrel{t^{\prime }}{\to })$. That conflicts with the liveness of $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$. Hence, there exist $S_0\prime \prime ,S_0\prime \prime \prime \in R\left(S_0\prime \right)$, such that $\Sigma =\left(Z,S_0\right)$ obtained from ($Z\prime ,S_0\prime \prime$) is live and ${\Sigma }_p=\left(Z_p,S_{p,0}\right)$ obtained from ($Z\prime \prime ,S_0\prime \prime \prime$) is live. Since $•\left(•p_{pin}\right)\in \{p{M}_0^{\prime }\left(p\right)>0\wedge p\in P\prime \}$, then $\Sigma =\left(Z,S_0\right)$ and $\overline{\Sigma }$ = ($\overline{Z_p}$, $\overline{S_{\mathrm{p},0}}$) are live. □

Theorem 4. 

Suppose that the PIRES+ net system $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is obtained from $\Sigma =\left(Z,S_0\right)$ by refinement operation Re $f_p\left(p_p,N_p\right)$. $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is bounded iff $\Sigma =\left(Z,S_0\right)$ and $\overline{\Sigma }$ = ($\overline{Z_p}$, $\overline{S_{p,0}}$) are bounded.

Proof. 

(If) Since $\Sigma =\left(Z,S_0\right)$ is bounded, $\forall p\in P,\exists k_1>0$ such that $\forall S\in R\left(S_0\right),M\left(p\right)\le k_1$. Obviously, $\forall p\in P-\left\{p_p\right\},M_{\left(P-\left\{p_p\right\}\right)}\left(p\right)\le k_1$. Since $\overline{\Sigma }$ = ($\overline{Z_p}$, $\overline{S_{\mathrm{p},0}}$) is bounded, then for every $p\in P_p,\exists k_2>0$, such that $\forall S_P\in R\left(S_{p_0}\right),M_P\left(p\right)\le k_2.$ Let $k=k_1+k_2$, by Definitions 12–15 and Supposition 1, $\forall p\in P^{\prime },\forall S^{\prime }\in R\left(S_0^{\prime }\right),M^{\prime }\left(p\right)=\left(M_{\left(P-\left\{p_p\right\}\right)},M_p\right)\left(p\right)\le k.$ By Definition 24, $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is bounded.

(Only-if) Without loss of generality, suppose $\Sigma =\left(Z,S_0\right)$ is not bounded, such that $\exists p\in P,\forall k>0,\exists S\in R\left(S_0\right), M\left(p\right)>k$. By Definitions 12–14, and Supposition 1, $\forall k>0,\exists S^{\prime }\in R\left(S_0^{\prime }\right), M\prime \left(p\right)>k$. That conflicts with the fact that $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is bounded.

Note that, by Supposition 2, Definitions 15, 16, and Theorems 3 and 4, we can investigate the preservation of liveness and boundedness of the PIRES+ place set refinement operation. □

Theorem 5. 

Suppose $P_p=\left\{p_1,p_2,\dots \dots , p_m\right\}\left(m\ge 2\right)$ is the PIRES+ place set of $N$, and $\forall p_i,p_j\in P_p$ (where $i\ne j$), $•p_i\cap •p_j$ = $\varnothing$ and $p_i•\cap p_j•$ = $\varnothing$. Let $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ be obtained from $\Sigma =\left(Z,S_0\right)$ using the PIRES+ place set refinement operation Re$f_{p_{set}}\left(P_{set},N_{set}\right)$. If $•\left(•p_{p_{pjin}}\right)\in \left\{p\left|{M^{\prime }}_0\left(p\right)\right.〉0\wedge p\in P\prime \right\}$ (where $j=1,2,3,\dots \dots ,m$), then $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is live if and only if $\Sigma =\left(Z,S_0\right)$ and $\overline{{\Sigma }_{pj}}=\left(\overline{Z_{pj}},\overline{S_{pj0}}\right)$ (where $j=1,2,3,\dots \dots ,m$) are live.

Proof. 

Since $P_p=\left\{p_1,p_2,\dots \dots ,p_m\right\}\left(m\ge 2\right)$ is the place set of $N$, and $\forall p_i,p_j\in P_p$ (where $i\ne j$), $•p_i\cap •p_j$ = $\varnothing$ and $p_i•\cap p_j•$ = $\varnothing$, we can refine the places of $P_p$ one by one. First, let ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$ be obtained from $\Sigma =\left(Z,S_0\right)$ using $N_{p1}$ to replace $p_1$ of $\Sigma =\left(Z,S_0\right)$. Since $•\left(•p_{p_{p1in}}\right)\in \{p{M}_0\prime \left(p\right)>0\wedge p\in P\prime \}$, by the proof process of Theorem 3, ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$ is live if and only if $\Sigma =\left(Z,S_0\right)$ and $\overline{{\mathsf{\Sigma }}_{p1}}=\left(\overline{Z_{p1}},\overline{S_{p10}}\right)$ are live. Second, let ${\Sigma }_2=\left(Z_2,S_{2,0}\right)$ be obtained from ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$ using $N_{p2}$ to replace $p_2$ of ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$. Since $•\left(•p_{p_{p2in}}\right)\in \{p{M}_{10}\prime \left(p\right)>0\wedge p\in P\prime \}$, by the proof process of Theorem 3, ${\Sigma }_2=\left(Z_2,S_{2,0}\right)$ is live if and only if ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$ and $\overline{{\mathsf{\Sigma }}_{p2}}=\left(\overline{Z_{p2}},\overline{S_{p20}}\right)$ are live. In the case of $p_3,\dots \dots ,p_m$, we can prove it in the same way. So, $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is live if and only if $\Sigma =\left(Z,S_0\right)$ and $\overline{{\mathsf{\Sigma }}_{pj}}=\left(\overline{Z_{pj}},\overline{S_{pj0}}\right)$ (where $j=1,2,3,\dots \dots ,m$) are live. □

Theorem 6. 

Suppose $P_p=\left\{p_1,p_2,\dots \dots ,p_m\right\}\left(m\ge 2\right)$ is the place set of $N$, and $\forall p_i,p_j\in P_p$ (where $i\ne j$), $•p_i\cap •p_j$ = $\varnothing$ and $p_i•\cap p_j•$ = $\varnothing$. Let $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ be obtained from $\Sigma =\left(Z,S_0\right)$ using the PIRES+ place set refinement operation Re$f_{p_{set}}\left(P_{set},N_{set}\right)$. $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is bounded if and only if $\Sigma =\left(Z,S_0\right)$ and $\overline{{\Sigma }_{pj}}=\left(\overline{Z_{pj}},\overline{S_{pj0}}\right)$ (where $j=1,2,3,\dots \dots ,m$) are bounded.

Proof. 

Since $P_p=\left\{p_1,p_2,\dots \dots ,p_m\right\}\left(m\ge 2\right)$ is the place set of $N$, and $\forall p_i,p_j\in P_p$ (where $i\ne j$), $•p_i\cap •p_j$ = $\varnothing$ and $p_i•\cap p_j•$ = $\varnothing$, we can refine these places $p_1,p_2,\dots \dots ,p_m$ one by one. First, let ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$ be obtained from $\Sigma =\left(Z,S_0\right)$ using $N_{p1}$ to replace $p_1$ of $\Sigma =\left(Z,S_0\right)$. By the proof process of Theorem 4, ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$ is bounded if and only if $\Sigma =\left(Z,S_0\right)$ and $\overline{{\mathsf{\Sigma }}_{p1}}=\left(\overline{Z_{p1}},\overline{S_{p10}}\right)$ are bounded. Second, let ${\Sigma }_2=\left(Z_2,S_{2,0}\right)$ be obtained from ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$ using $N_{p2}$ to replace $p_2$ of ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$. By the proof process of Theorem 4, ${\Sigma }_2=\left(Z_2,S_{2,0}\right)$ is bounded if and only if ${\Sigma }_1=\left(Z_1,S_{1,0}\right)$ and $\overline{{\mathsf{\Sigma }}_{p2}}=\left(\overline{Z_{p2}},\overline{S_{p20}}\right)$ are bounded. In the case of $p_3,\dots \dots ,p_m$, we can prove it in the same way. So, $\Sigma \prime =\left(Z\prime ,S_0\prime \right)$ is bounded if and only if $\Sigma =\left(Z,S_0\right)$ and $\overline{{\mathsf{\Sigma }}_{pj}}=\left(\overline{Z_{pj}},\overline{S_{pj0}}\right)$ (where $j=1,2,3,\dots \dots ,m$) are bounded. □

6. Application

The contribution of this work is to propose the place refinement operation and the place set refinement operation and verify the relevant important properties. To demonstrate the effectiveness of these refinement approaches, we use the refinement approaches for PIRES+ to model and analyze an embedded control system.

With the rapid development of communication technology, the frequency of communication technology innovation is gradually accelerating. 5G, as a new generation cellular mobile network, has its advantages of excellent wide area coverage, good mobility, low price, and high sharing of WLAN. In the actual network, cellular communication network and WLAN are two independent systems.

As we all know, WLAN is the product of the combination of computer network and wireless communication technology. It uses radio frequency technology (RF) to replace the old twisted pair to form a local area network. WLAN has many corresponding access specifications, all of which are in IEEE 802.11 standard. There is mainly a/b/ac/ad/n/ac. At present, 802.11.ac is widely used. When a piece of information is received through the wireless network, these information data are processed and decoded by the physical layer, data link layer, network layer, transport layer, and application layer, then restored to the most original information transmitted by the sender. We have simplified the structure of the transmission process, analyzed the whole information processing process from a macro perspective.

In order to effectively realize the real integration between heterogeneous networks, this section applies the refinement method of PIRES + proposed above to the modeling and analysis of mobile terminal network communication system. The refined operation of the network system can effectively achieve the integration of heterogeneous networks and accurately respond to the system workflow, and facilitate the future improvement and migration of the system. Next, the cellular mobile communication, WLAN network, and digital signal processing process of the mobile terminal network communication system will be modeled and analyzed.

6.1. Constructing a PIRES+ Model

We will construct an embedded control system’s PIRES+ model using the place set refinement operation. First, an abstract PIRES+ model of an embedded control subsystem will be presented. Second, the refined PIRES+ model is obtained using the PIRES+ refinement operations. The embedded control system’s abstract model ($N$) is illustrated in Figure 3.

In Figure 3, $p_1$: cellular network signal processing part; $p_7$: digital signal processing part; $p_{11}$: WLAN signal processing part.$t_1$: convert electromagnetic wave to RF-Radio Frequency;$t_2$: the baseband information is obtained by adjusting the filter;$t_3$: start digital signal processing;$t_4$: finish digital signal processing; $t_5$: pulse code modulation; $t_6$: verify WLAN signal password; $t_7$: the signal received from the antenna is converted into AC signal.

The subsystem $N_1$ is displayed in Figure 4. $N_1$ is the PIRES+ model of cellular network signal processing part.$t_{p11}$: adjust audio;$t_{p12}$: perform human-computer interaction;$t_{p13}$: finish current signal processing and initialize the system; $t_{p14}$: the antenna receives the electromagnetic wave signal sent by the base station. There exist transition functions $f_{p11},f_{p12},f_{p13},f_{p14}$ associated with transitions $t_{p11}$, $t_{p12}$, $t_{p13}$, $t_{p14}$, respectively. There exists transition set function $f_{p1}$ of subnet $N_1$, where $f_{p1}=$ $f_{p11}\circ$ $f_{p12}\circ f_{p13}\circ f_{p14}$. [$a_{p11},b_{p11}$], [$a_{p12},b_{p12}$], [$a_{p13},b_{p13}$], [$a_{p14},b_{p14}$], are transition delay intervals associated with transitions $t_{p11},t_{p12},t_{p13},$ $t_{p14}$ respectively. [$d_{p1}^{-},d_{p1}^{+}$] is the transition delay interval of subnet $N_1$, where $d_{p1}^{-}=a_{p11}+a_{p12}+a_{p13}+a_{p14}$, $d_{p1}^{+}=b_{p11}+b_{p12}+b_{p13}+b_{p14}$.

The subsystem $N_2$ is displayed in Figure 5. $N_2$ is the PIRES+ model of the digital signal processing part, where $t_{p21},t_{p22},t_{p23},t_{p24},t_{p25},t_{p26}$, represent a series of signal processing processes, such as acquisition, filtering, transformation, spectrum analysis, estimation, recognition, etc. There exist transition functions $f_{p21}$, $f_{p22}$, $f_{p23}$, $f_{p24}$, $f_{p25}$, $f_{p26}$, associated with transitions $t_{p21},t_{p22},t_{p23},t_{p24}$, $t_{p25},t_{p26}$, respectively. There exists transition set function $f_{p2}$ of subnet $N_2$, where $f_{p2}=f_{p21}\circ \left(\left(f_{p23}\parallel f_{p22}\right)\circ \left(f_{p24}\parallel f_{p25}\right)\right)\circ f_{p26}$. [$a_{p21},b_{p21}$], [$a_{p22},b_{p22}$], [$a_{p23},b_{p23}$], [$a_{p24},b_{p24}$], [$a_{p25},b_{p25}$], [$a_{p26},b_{p26}$] are transition delay intervals associated with transitions $t_{p21},t_{p22},t_{p23},t_{p24}$, $t_{p25},t_{p26}$, respectively. There exists transition delay interval [$d_{p2}^{-},d_{p2}^{+}$] of subnet $N_2$, where $d_{p2}^{-}=a_{p21}+\max \left(a_{p23}+a_{p24},a_{p22}+a_{p25}\right)+a_{p26},d_{p2}^{+}=b_{p21}+\max \left(b_{p22}+b_{p25},b_{p23}+b_{p24}\right)+b_{p26}$.

The subsystem $N_3$ is displayed in Figure 6. $N_3$ is the PIRES+ model of the WLAN signal processing part, where $t_{p31}$: human-computer interaction part;$t_{p32}$: finish the current signal processing and initialize the system; $t_{p33}$: the terminal receives WLAN signals from different sources. There exist transition functions $f_{p31}$, $f_{p32}$, $f_{p33}$, associated with transitions $t_{p31},t_{p32},t_{p33}$, respectively. There exists transition set function $f_{p3}$ of subnet $N_3$, where $f_{p3}=f_{p31}\circ f_{p32}\circ f_{p33}$. There exist transition delay intervals [$a_{p31},b_{p31}$], [$a_{p32},b_{p32}$], [$a_{p33},b_{p33}$] associated with transitions $t_{p31},t_{p32},t_{p33}$, respectively. [$d_{p3}^{-},d_{p3}^{+}$] is the transition delay interval of subnet $N_3$, where $d_{p3}^{-}=a_{p31}+a_{p32}+a_{p33}$, $d_{p3}^{+}=b_{p31}+b_{p32}+b_{p33}$.

The refined PIRES+ model $N\prime$ (Figure 7) is obtained using the refinement method. Place $p_1$, $p_7$, and $p_{11}$ of $N$ (Figure 3) are replaced by place subnet $N_1$, $N_2$, $\mathrm{and} N_3$, respectively.

In Figure 7, corresponding to place subnet $N_1$, the transition function of $t_5$ is $f_5\prime$, where $f_{p1}$ $\circ f_5\prime =f_5$. There exists a transition delay interval [$a_5^{\prime },b_5^{\prime }$] associated with transition $t_5$, where $d_{•p_{p11}}^{-}+d_{N_1}^{-}=d_{•p1}^{-}$, $d_{•p_{p11}}^{+}+d_{N_1}^{+}=d_{•p1}^{+}$, that is $a_5^{\prime }+d_{N_1}^{-}=a_5$, $b_5^{\prime }+d_{N_1}^{+}=b_5$. By place subnet $N_2$, the transition function of $t_3$ is $f_3\prime$, where $f_{p2}\circ f_3\prime =f_3$. There exists a transition delay [$a_3^{\prime },b_3^{\prime }$] associated with transition $t_3$, where $d_{•p_{p21}}^{-}+d_{N_2}^{-}=d_{•p7}^{-}$, $d_{•p_{p21}}^{+}+d_{N_2}^{+}=d_{•p7}^{+}$, that is, $a_3^{\prime }+d_{N_2}^{-}=a_3$, $b_3^{\prime }+d_{N_2}^{+}=b_3$. Corresponding to place subnet $N_3$, the transition function of $t_6$ is $f_6\prime$, where $f_{p6}\circ f_6\prime =f_6$. There exists a transition delay interval [$a_6^{\prime },b_6^{\prime }$] associated with transition $t_6$, where $d_{•p_{p31}}^{-}+d_{N_3}^{-}=d_{•p11}^{-}$, $d_{•p_{p31}}^{+}+d_{N_3}^{+}=d_{•p11}^{+}$, that is $a_6^{\prime }+d_{N_3}^{-}=a_6$, $b_6^{\prime }+d_{N_3}^{+}=b_6$.

6.2. Property Analysis of the PIRES+ Model

The preservation of several properties will be analyzed in this section.

6.2.1. Preservation of Reachability, Functionality, and Timing

Let PIRES+ subnet $N_{11}=\left(P_{11},T_{11},F_{I1},F_{O1},I_1,M_{1,0}\right)$ of $N$ (Figure 3), where $P_{11}=\left\{p_1,p_2,p_3,p_8\right\}$, $T_{11}=\left\{t_1,t_5\right\}$, $F_{I1}=\left\{\left(p_1,t_1\right),\left(p_8,t_5\right)\right\}$, $F_{O1}=\{\left(t_1,p_2\right),\left(t_1,p_3\right), \left(t_5,p_1\right)$}, $I_1=\varnothing$, $M_{1,0}\left(p_8\right)\ne \varnothing$. Let $N_{12}=\left(P_{12}, T_{12},F_{I2},F_{O2},I_2,M_{2,0}\right)$, where $P_{12}=\left\{p_{p11},p_{p12}, p_{p13},p_{p14},p_{p15},p_{p16} ,p_2,p_3,p_8\right\}$, $T_{12}=${$t_1,t_{p11},t_{p12}$, $t_{p13}$, $t_{p14}$, $t_5$}, $F_{I2}=\{\left(p_{p11},t_{p11}\right),\left(p_{p12},t_{p12}\right), (p_{p13}, t_{p12}$) $\left( p_{p14},t_{p13}\right)$, ($p_{p15},t_{p14}$),($p_{p16},t_1$), $\left(p_8,t_5\right)$}, $F_{O2}=\{\left(t_1,p_2\right), \left(t_1,p_3\right), \left(t_5,p_{\mathrm{p}11}\right),\left(t_{p11},p_{p12}\right),\left(t_{p11},p_{p13}\right)$, $\left(t_{p12}, p_{p14}\right), \left(t_{p13},p_{p15}\right), \left(t_{p14},p_{p16}\right)\}, I_2=\varnothing , M_{2,0}\left(p_8\right)\ne \varnothing$.

Let PIRES+ subnet $N_{21}=\left(P_{21},T_{21},F_{I3},F_{O3},I_3,M_{3,0}\right)$ of $N$ (Figure 3), where $P_{21}=\left\{p_4,p_5,p_6,p_7,p_9,p_8,p_{10}\right\}$, $T_{21}=\left\{t_3,t_4\right\}$, $F_{I3}=\left\{\left(p_4,t_3\right),\left(p_5,t_3\right),\left(p_6,t_3\right),\left(p_7,t_4\right)\right\}$, $F_{O3}=\{(t_3,p_7$) $\left(t_4,p_8\right),\left(t_4,p_9\right),\left(t_4,p_{10}\right), I_3=\varnothing ,M_{3,0}=\varnothing$; Let $N_{22}=\left(P_{22},T_{22}, F_{I4}, F_{O4},I_4, M_{4,0}\right)$, where $P_{22}$ = $\{p_4, p_5, p_6, p_9, p_{10}, p_{p21}, p_{p22}, p_{p23}, p_{p24}, p_{p25}, p_{p26}, p_{p27},p_{p28},p_8$}, $T_{22}=\left\{t_{p21},t_{p22},t_{p23},t_{p24},t_3,t_{p26},t_{25},t_4,\right\}$, $F_{I4}=\left\{\left(p_4,t_3\right),\left(p_5,t_3\right),\left(p_6,t_3\right),\left(p_{p28},t_4\right),\left(p_{p21},t_{p21}\right),\left( p_{p22},t_{p23}\right), \left(p_{p23},t_{p22}\right), \left(p_{p24}, t_{p24}\right), \left(p_{p25},t_{p25}\right),\left(p_{p26}, t_{p26}\right),\left(p_{p27},t_{p26}\right)\right\}$, $F_{O4}=\{\left(t_3,p_{p21}\right),\left(t_4,p_8\right)$, $\left(t_4,p_9\right), \left(t_4,p_{10}\right)$, ($t_{p21},p_{p22}), \left(t_{p21},p_{p23}\right)$, $\left(t_{p23},p_{p24}\right)$, $(t_{p22}$, $p_{p24})$, $\left(t_{p22},p_{p25}\right),\left(t_{p24}, p_{p26}\right)$, ($t_{p25},p_{p27}),\left(t_{p26},p_{p28}\right)$}, $I_4=\left\{\left(p_{p23},t_{p23}\right),\left(p_{p25},t_{p24}\right)\right\}$, $M_{4,0}=\varnothing$.

Let PIRES+ subnet $N_{31}=\left(P_{31},T_{31},F_{I5},F_{O5},I_5,M_{5,0}\right)$ of $N$ (Figure 3), where $P_{31}=\{p_{10},p_9,p_{11}$, $p_{12}$}, $T_{31}=\left\{t_6,t_7\right\}$, $F_{I5}=\left\{\left(p_{10},t_6\right),\left(p_9,t_6\right),\left(p_{11},t_7\right)\right\}$, $F_{O5}=\left\{\left(t_6,p_{11}\right),\left(t_7,p_{12}\right)\right\}, I_5=\varnothing$, $M_{5,0}$ ($p_{11})\ne \varnothing$. Let $N_{32}=$ ($P_{32},T_{32},F_{I6}, F_{O6},I_6,M_{6,0})$, where $P_{32}=\{p_{12},p_{p31},p_{p32}, p_{p33},p_9,p_{p34},p_{p35}$, $p_{10}\}$, $T_{32}=\{t_{p31},t_{p32}, t_{p33}, t_6, t_7)$, $F_{I5}=\{\left(p_{p35},t_7\right), \left(p_{p31},t_{p31}\right),\left(p_{p32},t_{p32}\right),\left(p_{10},t_6\right)$, $\left(p_{p34},t_{p33}\right),\left(p_{p33},t_{p33}\right),(p_9,t_6$)}$, F_{O5}=\{\left(t_{p31},p_{p32}\right), \left(t_{p32},p_{p33}\right)$, ($t_{p32}$, $p_{p34}),\left(t_{p33},p_{p35}\right),\left(t_7,p_{12}\right),\left(t_6,p_{p31}\right)\}$, $I_6=\varnothing$, $M_{6,0}\left(p_{p31}\right)\ne \varnothing$.

$N\prime$ is obtained from $N$ by the place set refinement method, that is, $p_1$ is replaced by $N_1$, $p_7$ is replaced by $N_2$, and $p_{11}$ is replaced by $N_3$. According to Figure 3, Figure 4, Figure 5, Figure 6 and Figure 7, ① $f_{p1}\circ f_5\prime =f_5$, $f_{p2}\circ f_3^{\prime }=f_3 ,\mathrm{and} f_{p3}\circ f_6\prime =f_6$; ② $d_{•p_{p11}}^{-}+d_{N_1}^{-}=d_{p1}^{-}$, $d_{•p_{p11}}^{+}+d_{N_1}^{+}=d_{p1}^{+}$, $d_{•p_{p21}}^{-}+d_{N_2}^{-}=d_{p4}^{-}$, $d_{•p_{p21}}^{+}+d_{N_2}^{+}=d_{p4}^{+}$, $d_{•p_{p31}}^{-}+d_{N_3}^{-}=d_{p7}^{-}$, $d_{•p_{p31}}^{+}+d_{N_3}^{+}=d_{p7}^{+}$; ③ $•p_1\cap •p_7=\varnothing$, $•p_1\cap •p_{11}=\varnothing$, $•p_7\cap •p_{11}=\varnothing$, $p_1•\cap p_7•=\varnothing$, $p_1•\cap p_{11}•=\varnothing$, $p_{11}•\cap p_7•=\varnothing$. By Theorem 2, $N\prime$ and $N$ have the same reachability, functionality, and timing.

6.2.2. Preservation of Liveness and Boundedness

Obviously, $\mathsf{\Sigma }=\left(Z,S_0\right)$ of $N$ (Figure 3) is live and bounded. According to the PIRES+ place set refinement operation, $\mathsf{\Sigma }\prime =\left(Z\prime ,S_0\prime \right)$ of $N\prime$ (Figure 7) is obtained from $\mathsf{\Sigma }=\left(Z,S_0\right)$, i.e., $p_1$ is replaced by place subnet $N_1$, $p_7$ is replaced by place subnet $N_2$, and $p_{11}$ is replaced by subnet $N_3$. Let $\overline{{\mathsf{\Sigma }}_{p1}}=\left(\overline{Z_{p1}},\overline{S_{p1,0}}\right)$ be the place-closed PIRES+ net system of $N_1$, $\overline{{\mathsf{\Sigma }}_{p2}}=\left(\overline{Z_{p2}},\overline{S_{p2,0}}\right)$ be the place-closed PIRES+ net system of $N_2$, $\overline{{\mathsf{\Sigma }}_{p3}}=\left(\overline{Z_{p3}},\overline{S_{p3,0}}\right)$ be the place-closed PIRES+ net system of $N_3$, By Definition 25 and the characteristics of subnets $N_1$, $N_2$ and $N_3$, $\overline{{\mathsf{\Sigma }}_{p1}}=\left(\overline{Z_{p1}},\overline{S_{p1,0}}\right)$, $\overline{{\mathsf{\Sigma }}_{p2}}=\left(\overline{Z_{p2}},\overline{S_{p2,0}}\right)$ and $\overline{{\mathsf{\Sigma }}_{p3}}=\left(\overline{Z_{p3}},\overline{S_{p3,0}}\right)$ are live and bounded. By Theorem 5 and Theorem 6, $\mathsf{\Sigma }\prime =\left(Z\prime ,S_0\prime \right)$ is live and bounded.

6.3. Summary of the Modeling

The above system has clear structural hierarchy, time characteristics, and task priority requirements, so it is difficult to model with ordinary Petri net, colored Petri net, or PRES+. First, this example establishes the overall simplified model of mobile terminal communication network system, cellular mobile communication model based on embedded system, WLAN network model, and other component models. Then, the refinement operation is carried out to obtain the overall system model. Finally, through formal analysis, it is proven that the refined net system preserves the reachability, functionality, timing, liveness, and boundedness of the original net system. This modeling method solves the problem of direct modeling difficulty caused by the complexity of the system and the portability loss of some components in the overall modeling. The example effectively illustrates the feasibility and practicability of the refinement operation proposed in this paper and provides a more practical theoretical basis for the modeling of some embedded systems.

7. Conclusions

Embedded systems are widely used in various devices and are becoming more and more complex with increasing requirements. To facilitate the verification and design of embedded systems, PIRES+ is introduced. PIRES+ has great expressive power and many applications in verification, modeling, and analysis of embedded systems.

However, the problem of state space explosion is a disadvantage for PIRES+’s ability to model, analyze, and verify large, complex systems. In order to resolve the state space explosion of Petri nets, there are three popular transformations in the literature, namely synthesis approach, refinement approach, and reduction approach. In order to model, analyze, and verify large complex embedded systems, and to solve PIRES+’s state space explosion problem, we have proposed the place refinement approach and the place set refinement approach for PIRES+. Compared with refinement methods for ordinary Petri nets, CPNs, and PRES+, these refinement methods can nicely describe certain characteristics of embedded systems. We have also investigated the property preservation of these refinement approaches. During the refining process, under certain constraints, reachability, timing, functionality, liveness, and boundedness will be preserved. The refinement methods for PIRES+ can be used to nicely resolve design problems of embedded systems.

Of course, the refinement operation methods proposed in this paper are only applicable to the operation of place in PIRES+, without considering the refinement operation of transition in PIRES+. At the same time, this paper only carries out qualitative research from the formal aspect, and lacks certain quantitative analysis and system simulation.

In the future, some quantitative analysis and system simulation for the PIRES+’s refinement operation should be studied. Other more general refinement, synthesis, or reduction approaches for PIRES+ should also be investigated, for example, a place-bordered refinement operation, or synthesis operation methods for PIRES+ and their applications.

Fuzzy linear programming [40,41] is a generalization of classical linear programming, which blurs the boundary of linear constraints. Under loose constraints, we can obtain the optimization conditions and optimization extremum. The combination of the fuzzy linear programming and the refinement operation may become another interesting research direction in the future.