Formal Modeling And Verification Of Information Transmission Mechanism In The Internet Of Vehicles Based On Extended PN

Petri Net is an important modeling tool in the field of formal verification.It has good graphical expression and strict mathematical analysis ability,which makes the expression of sequence,concurrency,and other relations of processes or components in the system more intuitive.After more than half a century of research,various high-level Petri Nets derived from Petri Nets are applied in various fields.With the rapid development of wireless communication technology,cloud computing technology,and sensor technology,large complex dynamic systems such as the Internet of Vehicles emerge in an endless stream.These systems play a pivotal role in the information age.Therefore,it is very important to formally model such complex systems,analyze and verify the established system model,and check the correctness,integrity,reachability,and other properties of the model.Large and complex dynamic systems often have complex model structures,which is easy to cause the state explosion problem due to the large state space of the model.Although advanced Petri Net systems such as Colored Petri Net,Time Petri Net,and Predicate/Transition Net can effectively alleviate the scale problem of the system model,the state space explosion problem still exists.Aiming at the above problems,this thesis takes the information transmission mechanism of the Internet of Vehicles as the application background and studies the formal modeling and verification of the interactive process of information transmission in the Internet of Vehicles.The main research contents of this thesis include:(1)Aiming at the problem of state space explosion in the modeling of large and complex dynamic systems such as the Internet of Vehicles,this thesis proposes the TPZN model which extends Time Petri Net and Z language and applies it to the formal modeling and analysis of information transmission mechanism of Internet of Vehicles.The completeness,reachability,and liveness analysis methods of the TPZN model are given.(2)According to the characteristics of the large number of nodes,dynamic topology,and real-time information transmission in a multi-source heterogeneous data environment,the information transmission mechanism of the Internet of Vehicles is formally modeled based on TPZN.The TPZN-Z language was used to formally describe the node equipment information and traffic rules in the information transmission mechanism model of the Internet of Vehicles,and the functional attributes and non-functional attributes of the model were depicted.TPZN-TPN was used to construct the information flow model of the information transmission mechanism of the Internet of Vehicles.(3)For the established formal model of the information transmission mechanism of the Internet of Vehicles in a multi-source heterogeneous data environment,the integrity,reachable and liveness of the model are analyzed and verified by using the formal analysis and verification method of the TPZN model,and the information transmission mechanism model of Internet of Vehicles is analyzed by Snoopy software simulation.This research content and experimental results show that the formal method can effectively avoid the state space explosion problem and reduce the analysis complexity of the model by simplifying the structure of the system net model and improving the safety of large complex dynamic systems.