# Formal Verification on the Safety of Internet of Vehicles Based on TPN andZ

Authors: Yang Liu; Liyuan Huang; Jingwei Chen
Journal: Mathematical Problems in Engineering
 (2020)

---

## Abstract

Nowadays, the Internet of Vehicles has become the focus of global technological innovation and transformation in the automotive industry. Its flow modelling appears to play a very important role for designing and controlling the transportation systems, since it is not only necessary for improving safety and transportation efficiency but also can yield a series of society, economy, and ecosystem environment problems. Considering the characteristics of the frame structure includes states and actions and discrete and continuous aspects of traffic flow dynamics, both petri net andZ have proved to be useful tools for modelling the Internet of Vehicles. It can formally describe the vehicle behavior accurately with petri net and more details with Z frame structure. A new integration formal method of time petri net and Z is presented in this paper for modelling the vehicle behaviors and traffic rules through taking into account state dependencies on external rules. Moreover, a case study in the Internet of Vehicles is proposed to deal with the accurate localization of events. It shows that this formal verification methods significantly improves the safety and intelligence of the Internet of Vehicles.


---

## Body

## 1. Introduction

With the development of communication technology, wireless sensing technology, automatics, artificial intelligence, and so on, the Internet of Vehicles techniques come out. It is the achievements combined with the latest technological of computers and the modern automobile industry. Because of the complex and dynamic environment when it is working, the control system becomes more and more complex. Since it is about life, the key safety factor, such as automotive engine, air bag control, brake system, sensor monitoring system, and traffic regulations, have very strict reliability requirements. Internet of Vehicles has made our life convenient; nevertheless, at the same time, accidents still happen often. Many researchers ensure the safety from different aspects [1–3] by different methods, such as control strategy, security factor, and intelligent platform. More and more experiences show that the formal method is very effective to ensure the safety of the Internet of Vehicles [4–7] systems.In fact, the formal method is a good way to inspect the problems in system design or requirement design [8, 9]. The running environment of the Internet of Vehicles is very complex and changes dynamically. It is hard to describe the Internet of Vehicle using only one single formal language. The traditional process analysis methods, such as Petri nets [10], CCS (Calculus of Communicating Systems) [11, 12], and CSP (Communication Sequential Processes) [13, 14], can model different aspects of the system from different angles and abstractions, but the powers of description for functional and nonfunctional attribute and constraint condition are deficient. The traditional model languages such as V [15, 16], B [17], and Z [18, 20] are good at modelling description, but poor at describing system concurrency. At present, the integrated specification languages are a hot topic, which produced CSPZ [21], TCOZ [22], PZN [23, 24], and so on. However, it seems that these languages do not aim at the Internet of Vehicles. PZN has a good advantage in describing traditional systems, since specification Z has a good frame structure both in state description and operation description, and Petri nets [25–28] are very suitable to express the behavior of the parallel and concurrent system model. So, the hybrid methodology which combines the advantages of both specification Z and Petri nets is very suitable for modelling and analyzing the Internet of Vehicles system. PZN has been used to model and analyze validity and accessibility of networked software. Experimental results showed that PZN is very suitable to apply in it. In the Internet of Vehicles circumstance, except states and operation, time constraint is also very important. It not only has continuous part time but also has discrete time. Some researchers used time Petri nets to model the requirements and software of system [29–34], but it lacked specific rule descriptions and state depictions.Motivated by the previous experience in formal verification of requirements modelling and analyzing of networked software, in this paper, TPZN (integration Time Petri Net andZ) is proposed to formal modelling and verifying the Internet of Vehicles systems. It is able to describe the concurrent process and fore-and-aft states in systems at different times. TPZN consists of two parts TPZN-TPN and TPZN-Z. TPZN-TPN defines the data flow of the whole structure, order, and behavior of process at one moment, while, TPZN-Z depicts the abstract data frame, specific rule restriction, and time constraint. So, based on enhancing the abstraction of the data and refinements by Z, the number of states of the Time Petri Nets can be decreased effectively. A case study shows the modelling method in detail. This formal method is proved greatly by improving the safety and validity of the intelligent vehicle systems.


## 2. Background

In this section, we recall some preliminary backgrounds that are necessary for the rest of the paper.


### 2.1. Hybrid Petri Net Extension

Hybrid petri net extension for traffic road modelling is proposed by Riouali et al. in [7]. It brought discrete parts and continuous parts which include discrete and continuous places and transitions. The moving and evolution of the Internet of Vehicles depend on the state of places and are governed by various function, namely, creation, destruction, merging, and splitting; meanwhile, it defined the speed, maximum density, length, and maximum flow of the traffic road modelling.A hybrid petri net consists of three kinds of objects: places, transitions, and directed arcs. However, unlike the traditional petri net, here places are divided into two kinds: discrete places and continuous places. Transitions as well as places also fall into discrete transitions and continuous transitions. Arcs still show the state dynamic from places to transitions or from transitions to places. Hybrid petri net extension is defined 6-tupletN = (P, T, Pre, Post, Υ, Time).(1)
P is a set of places, P = Pc ∪ Pd, where Pc represents continuous places and Pd represents discrete places.(2)
T is a set of transitions.(3)
Pre is the backward incidence matrixP×T⟶N.(4)
Post is the forward incidence matrixT×P⟶N.(5)
γ represents the batch place function. It associates with each batch place 4-tuplet (Vi: speed; di: a maximum density; Si: length; Φmax: a maximum flow).(6)
Time represents the firing delay in case of continuous or batch transitions.Here, we consider the time factor, while theγ is more suitable to be used in more intelligent vehicle concurrent environment.


### 2.2. Z Frame Structure

Z is a good formalism for modelling and designing. Compared with Petri Net,Z has better abilities in type definition and data abstraction and model refining. Its basic frame contains states and operations as Figure 1. Every operation has relative states and constrain rules. However, it does not describe the dynamic behavior of the systems.Figure 1
Frame structure of Z.Although Ding et al. and Wei et al. proposed a method that models systems by bothZ and Petri Nets in [27, 28] and the authors also showed that using PZN (Z and Petri Nets) to model the requirements of software is an effective and feasible way [9], it is still not good enough to model the Internet of Vehicles. The reason is that PZN does not have the ability to describe the real-time performance which is very important in vehicle systems. In transportation systems, time is a very important factor. So, all previous works have to be improved and time constraints will be added in PZN [9]. TPZN stands for the integration of PZN and time factor. In Section 3, we will introduce the modelling and analysis methods by TPZN.


## 2.1. Hybrid Petri Net Extension

Hybrid petri net extension for traffic road modelling is proposed by Riouali et al. in [7]. It brought discrete parts and continuous parts which include discrete and continuous places and transitions. The moving and evolution of the Internet of Vehicles depend on the state of places and are governed by various function, namely, creation, destruction, merging, and splitting; meanwhile, it defined the speed, maximum density, length, and maximum flow of the traffic road modelling.A hybrid petri net consists of three kinds of objects: places, transitions, and directed arcs. However, unlike the traditional petri net, here places are divided into two kinds: discrete places and continuous places. Transitions as well as places also fall into discrete transitions and continuous transitions. Arcs still show the state dynamic from places to transitions or from transitions to places. Hybrid petri net extension is defined 6-tupletN = (P, T, Pre, Post, Υ, Time).(1)
P is a set of places, P = Pc ∪ Pd, where Pc represents continuous places and Pd represents discrete places.(2)
T is a set of transitions.(3)
Pre is the backward incidence matrixP×T⟶N.(4)
Post is the forward incidence matrixT×P⟶N.(5)
γ represents the batch place function. It associates with each batch place 4-tuplet (Vi: speed; di: a maximum density; Si: length; Φmax: a maximum flow).(6)
Time represents the firing delay in case of continuous or batch transitions.Here, we consider the time factor, while theγ is more suitable to be used in more intelligent vehicle concurrent environment.


## 2.2. Z Frame Structure

Z is a good formalism for modelling and designing. Compared with Petri Net,Z has better abilities in type definition and data abstraction and model refining. Its basic frame contains states and operations as Figure 1. Every operation has relative states and constrain rules. However, it does not describe the dynamic behavior of the systems.Figure 1
Frame structure of Z.Although Ding et al. and Wei et al. proposed a method that models systems by bothZ and Petri Nets in [27, 28] and the authors also showed that using PZN (Z and Petri Nets) to model the requirements of software is an effective and feasible way [9], it is still not good enough to model the Internet of Vehicles. The reason is that PZN does not have the ability to describe the real-time performance which is very important in vehicle systems. In transportation systems, time is a very important factor. So, all previous works have to be improved and time constraints will be added in PZN [9]. TPZN stands for the integration of PZN and time factor. In Section 3, we will introduce the modelling and analysis methods by TPZN.


## 3. Modelling with TPZN

For satisfying the real-time capability and dynamic evolution and data abstraction and type definition capabilities of the Internet of Vehicles, the integrated specification TPZN is presented in this paper. Based on enhancing the abstraction of the data and refinements byZ, the state-of-the-time Petri Nets can be decreased effectively. Compared with time petri nets, color petri nets, PZN, and CSPZ, TPZN is more suitable to define the intelligent vehicle systems.


### 3.1. TPZN

Definition 1.
A TPZN is a tuple <P, T, F, Zp, ZT, S, C, M0, SI>, where(1)
P is a set of the states.(2)
T is a set of the transitions.(3)
F is a set of the arcs which links state and transition.(4)
N  = (P, T, F) is a SISO net.(5)
TPN = (P, T, F, M0, SI) is like a traditional time petri net.(6)
PZN = (P, T, F, Zp, ZT, S, C) is a PZN as in [9, 19].(7)
Zp is a set of the state frame based on Z.(8)
ZT is a set of the operation frame based on Z.(9)
S: P⟶Zp is a set of the one-to-one map relationship between P and Zp.(10)
C: T⟶ZT is a set of the one-to-one map relationship between T and ZT.(11)
M0: is the initial mark, and ∃t∈T,p0,t∈F,M0t>.(12)
∃ω,ω∈LTPN,φfTPN,ω=Mf,Df,SIf,M0=pi+pj+⋯+pk,D0=D0tm,D0tn,…, SI0=0,0, pi,pj,…,pk are all trigger states in the beginning and tm,tn,…are all trigger transitions.Mf represents the state of every node device in one time. Df represents a set of the time interval of the next possible transition. SIf represents the time interval of the system may need when it arrives Mf. φf represents the system’s situation during time interval-SIf. If Mf is the final state, Df=∅.
To ensure the compatibility and validity of the design, TPZN-Z frame is used to describe the sign, property, rules, and so on. The corresponding relation of TPN andZ is shown in Figure 2. The green dashed box is the precondition of transition. The rules and constraints are formally described by Z in Zt. The purple dashed box represents the postcondition by Z.Figure 2
The relation between TPN and Z in TPZN.


### 3.2. Time Constrained in TPZN

This paper introduces global time and relative time for TPZN. The global time proves the standard system time, and the relative time supplies the time relative to previous statusMi. Here, it needs to define two variables. One is the earliest occurrence time, EAR(t), the other one is the latest occurrence time, LAT(t). SIi contains the earliest occurrence time EAR(ti) and the latest occurrence time LAT(ti). SIi=EARti,LATti. Di(t) is the relative time to Mi-1, Mi−1ti>.For example, in Figure3, relative time is marked. For example, “t7 [15, 25]” means that t7 can be triggered in 15 seconds at least and 25 seconds at most. If it exceeds 25 seconds, the automatic delivery truck will stop working. Accordingly, the system will be warning. The global time is always synchronized with the time of the system.Figure 3
The TPZN of automatic delivery truck.


### 3.3. Model Refining

The environment of the Internet of Vehicles running is always complex, dynamic, and unexpected so that model refining and topological evolution capability is to be very important. SupposeTPZN11and TPZN12 are the subnet of TPZN1:(1)TPZN11=P11,T11,F11,Zp11,ZT11,S11,C11,M011,SI11,TPZN12=P12,T12,F12,Zp12,ZT12,S12,C12,M012,SI12.Then,TPZN11∩TPZN12⊂TPZN1. ∀pi,pi∈P,P∈TPZN11/TPZN11∩TPZN12 are all the new additional virtual states which represent the possible states before or after the subnet TPZN11. ∀ti,ti∈T,T∈TPZN11/TPZN11∩TPZN12 are all the new additional virtual transitions which represent the possible preconditions or postconditions. Of course, new Z frame structure Zp′ and Zt′ should be redefined by additional rules. In the similar way, a new TPZN′ can substitute a transition ti, when the control structure change.On the contrary, when one model is needed to be abstracted, it can be seen as a new transitiont′; then adding its precondition and postcondition and reserving input and output are relative to the conterminal model.Theorem 1.
If the global execution time of every transition sequence of the new refined TPZN model from the beginning to the end is equal to the execution time of the substitutedti of the original TPZN, the new refined TPZN can maintain behavioral consistency with the original one.Because TPZN integrates TPN and Z, the refined TPN can maintain behavioral consistency with the original one and has been proved in [35–37].


## 3.1. TPZN

Definition 1.
A TPZN is a tuple <P, T, F, Zp, ZT, S, C, M0, SI>, where(1)
P is a set of the states.(2)
T is a set of the transitions.(3)
F is a set of the arcs which links state and transition.(4)
N  = (P, T, F) is a SISO net.(5)
TPN = (P, T, F, M0, SI) is like a traditional time petri net.(6)
PZN = (P, T, F, Zp, ZT, S, C) is a PZN as in [9, 19].(7)
Zp is a set of the state frame based on Z.(8)
ZT is a set of the operation frame based on Z.(9)
S: P⟶Zp is a set of the one-to-one map relationship between P and Zp.(10)
C: T⟶ZT is a set of the one-to-one map relationship between T and ZT.(11)
M0: is the initial mark, and ∃t∈T,p0,t∈F,M0t>.(12)
∃ω,ω∈LTPN,φfTPN,ω=Mf,Df,SIf,M0=pi+pj+⋯+pk,D0=D0tm,D0tn,…, SI0=0,0, pi,pj,…,pk are all trigger states in the beginning and tm,tn,…are all trigger transitions.Mf represents the state of every node device in one time. Df represents a set of the time interval of the next possible transition. SIf represents the time interval of the system may need when it arrives Mf. φf represents the system’s situation during time interval-SIf. If Mf is the final state, Df=∅.
To ensure the compatibility and validity of the design, TPZN-Z frame is used to describe the sign, property, rules, and so on. The corresponding relation of TPN andZ is shown in Figure 2. The green dashed box is the precondition of transition. The rules and constraints are formally described by Z in Zt. The purple dashed box represents the postcondition by Z.Figure 2
The relation between TPN and Z in TPZN.


## 3.2. Time Constrained in TPZN

This paper introduces global time and relative time for TPZN. The global time proves the standard system time, and the relative time supplies the time relative to previous statusMi. Here, it needs to define two variables. One is the earliest occurrence time, EAR(t), the other one is the latest occurrence time, LAT(t). SIi contains the earliest occurrence time EAR(ti) and the latest occurrence time LAT(ti). SIi=EARti,LATti. Di(t) is the relative time to Mi-1, Mi−1ti>.For example, in Figure3, relative time is marked. For example, “t7 [15, 25]” means that t7 can be triggered in 15 seconds at least and 25 seconds at most. If it exceeds 25 seconds, the automatic delivery truck will stop working. Accordingly, the system will be warning. The global time is always synchronized with the time of the system.Figure 3
The TPZN of automatic delivery truck.


## 3.3. Model Refining

The environment of the Internet of Vehicles running is always complex, dynamic, and unexpected so that model refining and topological evolution capability is to be very important. SupposeTPZN11and TPZN12 are the subnet of TPZN1:(1)TPZN11=P11,T11,F11,Zp11,ZT11,S11,C11,M011,SI11,TPZN12=P12,T12,F12,Zp12,ZT12,S12,C12,M012,SI12.Then,TPZN11∩TPZN12⊂TPZN1. ∀pi,pi∈P,P∈TPZN11/TPZN11∩TPZN12 are all the new additional virtual states which represent the possible states before or after the subnet TPZN11. ∀ti,ti∈T,T∈TPZN11/TPZN11∩TPZN12 are all the new additional virtual transitions which represent the possible preconditions or postconditions. Of course, new Z frame structure Zp′ and Zt′ should be redefined by additional rules. In the similar way, a new TPZN′ can substitute a transition ti, when the control structure change.On the contrary, when one model is needed to be abstracted, it can be seen as a new transitiont′; then adding its precondition and postcondition and reserving input and output are relative to the conterminal model.Theorem 1.
If the global execution time of every transition sequence of the new refined TPZN model from the beginning to the end is equal to the execution time of the substitutedti of the original TPZN, the new refined TPZN can maintain behavioral consistency with the original one.Because TPZN integrates TPN and Z, the refined TPN can maintain behavioral consistency with the original one and has been proved in [35–37].


## 4. Modelling Analysis

### 4.1. Accessibility

Traditionally speaking, there are two ways to analysis the accessibility of the model. One way is using the reachability tree which is used to analysis the accessibility of model states. Because the accessibility of the TPZN involves limited time and there are lots of the state classes, some methods to reduce the state classes are necessary. For instance, Bourdil and Berthomieu have proposed some methods to reduce the state classes [28, 31]. Based on their work, we use Z frame to abstract the system so to reduce the state number. The layer can be subdivided into smaller layers. If the lowest layers can be verified to be correct, accessible, and safe, the whole upper layer will have the same character. The reachability tree can be built by φf based on TPZN. From φfi to φfj, the path from the node φfi of the tree to the node φfj shows the transition sequence (Figure 4).Figure 4
The TPZN of automatic delivery truck.The other way is using the incidence matrix markedC(C = D+ − D−). Here, the output matrix-D+ is defined as(2)D+i,j=0,∄fk=ti,pj,fk∈T×P,n,∃fk=ti,pj,fk∈T×P∧TokenPj=n,where D+[i, j] = 0 means there does not exist an arc from the ti to pj. While, D+[i, j] = n means that there is an arc from the ti to pj, and it will produce n same type elements with the transfer. The (i, j) entry of D- is defined as(3)D−i,j=0,∄fk=pi,tj,fk∈P×T,n,∃fk=pi,tj,fk∈P×T∧TokenPi=n>tj,where D−[i, j] = 0 means there is not an arc from the pi to tj, while D−[i, j] = n means that there is an arc from the pi to tj and the transition can happen only if there is n same type elements in the pj.SupposingMi is a marked state. From Mi to Mj, if there is an transition sequences σ=titi+1,…,tj marked by X-vector quantity and it satisfies Mj=Mi+X•D+−D−, it proves that the Mi state is accessibility. However, in TPZN, it must consider the limited time. The time constrained rules are described by Z frame. In the automotive vehicles system, time constrained rules must be built strictly because subtle time change may cause serious traffic accident. So, modelling the vehicles’ system, it needs to abstract the whole system, then subdivide the whole system into specific layers, and go on subdividing until it is subdivided into atom modules. By φf which represents the state class containing timestamp, we can get the possible behavior information of the system in certain time interval and then predict the next step. The algorithm of accessibility is designed as Algorithm 1 which shows the accessibility decision from Mi to Mj, and the case study explains how to use it in Figure 5.Algorithm 1: The algorithm of accessibility. Accessibility decision from Mi to Mj.
Input:φf=φf0,φf1,φf2,…,φfe, Mi, Mj, D+, D−Output: true (print the path); falseFind theX, X = Mj−Mi•D+−D−−1IfX not exist, return false;ElseFor (k = 0; k< n; k++)σk=th,th+1,…,th+c;//σk store the different value of X, n is the number of X.φf0 is the root node;//built the reachability treeFor (k = 1; k ≤ e; k++){if (∃tm,tm∈T, Mk>tm ) ∧SIk⋅EARtk,SIk⋅LARtk⊆systemt+intervaltimetkφfk is the child node of φfk−1 ;}//test the time constrainFor(k = 0; k< n; k++){If (σk=th,th+1,…,th+c) exist in one path of φfi to φfj,Lookup(S, C); //find the relative Zp′ and ZT′, test the logical relationshipIf the logical relationship fromZpa,Zpb,…,ZpdMi=Pa+Pb+⋯+Pd,Zpa,Zpb,…,Zpd∈Zp′ to Zpe,Zpf,…,ZprMj=Zpe+Zpf+⋯+Zpr,Zpe,Zpf,…,Zpr∈Zp′ is reasoned to be correct.Printφfi,tn,φfi+1,tn+1,…,tn+c,φfj;}Figure 5
Reachability tree of the case study.


### 4.2. Validity

The validity of the control structure can be analyzed by the transfer matrixLDP of TPZN. From the LDP, concurrent transition can be obtained by the same column and row. As the following in LDP1, t1 and t2 can be trigger simultaneously from p0 to p1 and pe, while, if p1 is arrived, t1 and t3 must be triggered:(4)So, the data flow structure can be mapped into the transfer matrixLDP. If there exist several transitions in the same row pi, it means when the system arrives into the state pi, these transitions will be simultaneously triggered. While if there exist several transitions in the same column pi, it means only under the condition that all the transitions are triggered, and pi can be reached.After getting the initial model and parameters, the sampled data or historical data can be used to correct the model and parameters. Of course, real time data also can be used to modify the model and parameters, but more often, it is used to predict possible state of the future.The process of modelling the Internet of Vehicles with TPZN is as Figure6. First, the node device information and traffic rules and evaluation indicators are obtained from the initial system model. Meanwhile, the data flow structure of the system should be obtained, and divide the initial system into subsystem. Second, the foregoing information is described by Z frame structures, and the latter is described by TPN. Third, the subsystem should be refined. Then, the whole system can be formally modelled by TPZN. Next, the related parameters such as LDP, φf, D+, and D− can be obtained from the TPZN model. Combined with the current information of the system, the initial parameters are used to analyze the character. At last, the future behavior of the vehicle system can be predicted. If the prediction shows, it will be in danger, and some strategies can be adopted. If the danger is caused by some traffic rules, these rules will be modified.Figure 6
The flow diagram of modelling with TPZN.


### 4.3. Advantage

Compared with TPN, PZN, andZ, TPZN has better dynamic structure and more convenient time constraint which are very important to the Internet of Vehicles. Except these, TPZN has better frame structure which can abstract the system to reduce the number of the states to avoid the explosive growth usually happened in traditional Petri Net. So, the advantage of modelling with TPZN is shown very clearly in Table 1.Table 1
Compared TPZN, TPN, PZN, andZ.
Dynamic structureFrame structureNumber of statesTime constraintTPZNGoodGoodAbstractGoodTPNGoodNot goodExplosive growthGoodPZNGoodGoodAbstractNot goodZNot goodGoodAbstractNot good


## 4.1. Accessibility

Traditionally speaking, there are two ways to analysis the accessibility of the model. One way is using the reachability tree which is used to analysis the accessibility of model states. Because the accessibility of the TPZN involves limited time and there are lots of the state classes, some methods to reduce the state classes are necessary. For instance, Bourdil and Berthomieu have proposed some methods to reduce the state classes [28, 31]. Based on their work, we use Z frame to abstract the system so to reduce the state number. The layer can be subdivided into smaller layers. If the lowest layers can be verified to be correct, accessible, and safe, the whole upper layer will have the same character. The reachability tree can be built by φf based on TPZN. From φfi to φfj, the path from the node φfi of the tree to the node φfj shows the transition sequence (Figure 4).Figure 4
The TPZN of automatic delivery truck.The other way is using the incidence matrix markedC(C = D+ − D−). Here, the output matrix-D+ is defined as(2)D+i,j=0,∄fk=ti,pj,fk∈T×P,n,∃fk=ti,pj,fk∈T×P∧TokenPj=n,where D+[i, j] = 0 means there does not exist an arc from the ti to pj. While, D+[i, j] = n means that there is an arc from the ti to pj, and it will produce n same type elements with the transfer. The (i, j) entry of D- is defined as(3)D−i,j=0,∄fk=pi,tj,fk∈P×T,n,∃fk=pi,tj,fk∈P×T∧TokenPi=n>tj,where D−[i, j] = 0 means there is not an arc from the pi to tj, while D−[i, j] = n means that there is an arc from the pi to tj and the transition can happen only if there is n same type elements in the pj.SupposingMi is a marked state. From Mi to Mj, if there is an transition sequences σ=titi+1,…,tj marked by X-vector quantity and it satisfies Mj=Mi+X•D+−D−, it proves that the Mi state is accessibility. However, in TPZN, it must consider the limited time. The time constrained rules are described by Z frame. In the automotive vehicles system, time constrained rules must be built strictly because subtle time change may cause serious traffic accident. So, modelling the vehicles’ system, it needs to abstract the whole system, then subdivide the whole system into specific layers, and go on subdividing until it is subdivided into atom modules. By φf which represents the state class containing timestamp, we can get the possible behavior information of the system in certain time interval and then predict the next step. The algorithm of accessibility is designed as Algorithm 1 which shows the accessibility decision from Mi to Mj, and the case study explains how to use it in Figure 5.Algorithm 1: The algorithm of accessibility. Accessibility decision from Mi to Mj.
Input:φf=φf0,φf1,φf2,…,φfe, Mi, Mj, D+, D−Output: true (print the path); falseFind theX, X = Mj−Mi•D+−D−−1IfX not exist, return false;ElseFor (k = 0; k< n; k++)σk=th,th+1,…,th+c;//σk store the different value of X, n is the number of X.φf0 is the root node;//built the reachability treeFor (k = 1; k ≤ e; k++){if (∃tm,tm∈T, Mk>tm ) ∧SIk⋅EARtk,SIk⋅LARtk⊆systemt+intervaltimetkφfk is the child node of φfk−1 ;}//test the time constrainFor(k = 0; k< n; k++){If (σk=th,th+1,…,th+c) exist in one path of φfi to φfj,Lookup(S, C); //find the relative Zp′ and ZT′, test the logical relationshipIf the logical relationship fromZpa,Zpb,…,ZpdMi=Pa+Pb+⋯+Pd,Zpa,Zpb,…,Zpd∈Zp′ to Zpe,Zpf,…,ZprMj=Zpe+Zpf+⋯+Zpr,Zpe,Zpf,…,Zpr∈Zp′ is reasoned to be correct.Printφfi,tn,φfi+1,tn+1,…,tn+c,φfj;}Figure 5
Reachability tree of the case study.


## 4.2. Validity

The validity of the control structure can be analyzed by the transfer matrixLDP of TPZN. From the LDP, concurrent transition can be obtained by the same column and row. As the following in LDP1, t1 and t2 can be trigger simultaneously from p0 to p1 and pe, while, if p1 is arrived, t1 and t3 must be triggered:(4)So, the data flow structure can be mapped into the transfer matrixLDP. If there exist several transitions in the same row pi, it means when the system arrives into the state pi, these transitions will be simultaneously triggered. While if there exist several transitions in the same column pi, it means only under the condition that all the transitions are triggered, and pi can be reached.After getting the initial model and parameters, the sampled data or historical data can be used to correct the model and parameters. Of course, real time data also can be used to modify the model and parameters, but more often, it is used to predict possible state of the future.The process of modelling the Internet of Vehicles with TPZN is as Figure6. First, the node device information and traffic rules and evaluation indicators are obtained from the initial system model. Meanwhile, the data flow structure of the system should be obtained, and divide the initial system into subsystem. Second, the foregoing information is described by Z frame structures, and the latter is described by TPN. Third, the subsystem should be refined. Then, the whole system can be formally modelled by TPZN. Next, the related parameters such as LDP, φf, D+, and D− can be obtained from the TPZN model. Combined with the current information of the system, the initial parameters are used to analyze the character. At last, the future behavior of the vehicle system can be predicted. If the prediction shows, it will be in danger, and some strategies can be adopted. If the danger is caused by some traffic rules, these rules will be modified.Figure 6
The flow diagram of modelling with TPZN.


## 4.3. Advantage

Compared with TPN, PZN, andZ, TPZN has better dynamic structure and more convenient time constraint which are very important to the Internet of Vehicles. Except these, TPZN has better frame structure which can abstract the system to reduce the number of the states to avoid the explosive growth usually happened in traditional Petri Net. So, the advantage of modelling with TPZN is shown very clearly in Table 1.Table 1
Compared TPZN, TPN, PZN, andZ.
Dynamic structureFrame structureNumber of statesTime constraintTPZNGoodGoodAbstractGoodTPNGoodNot goodExplosive growthGoodPZNGoodGoodAbstractNot goodZNot goodGoodAbstractNot good


## 5. A Case Study

To verify effectiveness of our modelling methods to analyze our verification algorithms, in this section, a simple case study is offered. Suppose that an intelligent car has 4 lidars, 4 radars, 4 side vision, 1 full vision, image processing system, radar system, lidar system, brake system, and so on. It is running on the straight road, as shown in Figure7.Figure 7
The environment of a case study.For modelling the system, the first step is to obtain theZ frame structure of every node device. Here, parts of the system model’s, such as Zp and Zt, are put forward as space is limited.The above frame is the same parts of one element of theZp, which is defined as one kind of state of the system. As the blue dashed box shows, it formally defines relative devices. The following one defines one node device of the system.The next frame is one element of theZt which defines one kind of possible transition of the system.So, at the first step, every node device’sZ frame structure and every transition can be defined. In second step, the TPN model of the Internet of Vehicles system will be built. Parts of the TPN model are shown in Figure 8.Figure 8
TPN model of the case study.Then, the TPZN of this case is <P, T, F, Zp, ZT, S, C, M0, SI>, where(1)
P=p0,p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16.(2)
T=t0,t1,t2,t3,t4,t5,t6,t7,t8,t9.(3)
F is the set of arcs in Figure8. The elements are like the following form p0,t0,t0,p1,t0,p2,t0,p3,t0,p4,t0,p5,p1,t1,….(4)
Zpi is the element of the set of Zp, and it represents the state of Z frame of the node devices as CAR and FrontLeftLi.(5)
Zti is the element of the set of ZT, and it represents the transition of Z frame of the system as BEGIN.(6)
S maps the relationship from state pi to Z frame of the state, as p0- > CAR.(7)
C maps the relationship from transition ti to Z frame of the transition, as t0- > BEGIN.(8)
M0=(1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0) represents the initial condition of the system.SIi is shown in Table 2, which represents the temporal interval under Mi. Some of the details of each pi and ti are shown as Table 3. Figure 7 shows parts of the case study, so, the p9 and p10 are not the real final states. In fact, p9 and p10 can turn into normal state by some steps.Table 2
The detail of SI.
IφfiMiDiSIii = 0M0,D0,SI0P0D0t0=5,300,0i = 1M1,D1,SI1P1+P2+P3+P4+P5+P12+P13D1t1=5.04,30.08,5,30D1t2=5.04,30.08,D1t3=5.05,30.1,D1t4=5.05,30.1,D1t7=5.03,30.1,D1t8=5.03,30.1i = 2M2,D2,SI2P7+P6+P14D2t6=5.06,30.65.05,30.01i = 3M3,D3,SI3P8+P11+P14D3t5=5.15,30.65.05,30.1i = 4M4,D4,SI4P8+P11+P15D4t9=5.06,30.125.05,30.1i = 5M5,D5,SI5P9∅5.35,30.6i = 6M6,D6,SI6P16∅5.06,30.12i = 7M7,D7,SI7P10∅5.15,30.6Table 3
The details of states and operations.
P0The start of intelligent carP14Obstacles, traffic light, and so onP1Lidar 1P15Normal environmentP2Lidar 2P16Keep runningP3Lidar 3t0StartP4Radar 1t1Processed normal data by lidar systemP5Radar 2t2Processed abnormal data by lidar systemP6Detected obstacles ahead by radart3Processed normal data by radar systemP7Detected obstacles ahead by lidart4Processed abnormal data by radar systemP8Detected normal environment by radart5DeceleratingP9Braket6BrakingP10Decelerationt7Process by vision-frontP11Detected normal environment by lidart8Process by wide-angleP12Vision-frontt9Check informationP13Wide-angleFrom Figure8, the final state classes are φf5, φf6,andφf7, where φf5 is the emergency brake, φf7is slow down, and φf6 is running straight normally. The transfer matrix LDP, D+, and D−of this case study is as follows:(5)From the matrixLDP, the concurrent behavior can be easily found. By the D+, D−, Mi, Mj, φfi, and φfj, the next behavior can be deduced exactly. The exact arrival time can also be obtained from SIi and SIj from the reachability tree as shown in Figure 5. The rules can be amended through the Zp and Ztwith the new data coming as well. Every Z frame structure can be coded by high-level programming language so to reason the logic relationship easily.


## 6. Conclusions

In this paper, we propose a new way that uses TPN andZ frame structure to formally model and analyze the safety and accessibility of the Internet of Vehicles. The method has been explained in detail by a case study. Although it promotes the efficiency of finding problem when the system goes wrong and can predict the future behavior, the multiple intelligent vehicles working cooperatively are not taken into account, which is an important and intriguing topic that we are working on.



---

*Source: 6618168-2020-12-29.xml*