Modeling And Analysis Of CPS Based On Extended Hybrid Petri Net

Cyber Physical System(CPS)is a complex system,which is composed of computing system,communication system,perceptual system,control system,and physical system.It realizes the effective control to physical process through the dynamic perception of physical environment and resources,the real-time and reliable transmission of information,the comprehensive calculation of data processing,and the use of feedback loops.Running of CPS is a kind of hybrid behavior that contains discrete computing process and continuous physical process are closely interacted and deeply integrated.Petri net,as a network of using token flow to represent the dynamic changes,is suitable for describing kind of systems with the feature of concurrent,asynchronous,uncertain and so on.Traditional Petri net is a discrete model,which cannot describe the evolution of continuous variables.Hybrid Petri net is one of the powerful tools for modeling hybrid systems.On this basis,we propose an extended hybrid Petri net model.With the increasing application of CPS in the field of security,such as aerospace,industrial control,medical equipment,et al,the demands of the safety and reliability of system are also increasing,so how to ensure the reliability of system is one of the most important problems.Focusing on the modeling and analysis of CPS,specific work is as follows: First,for discrete and continuous integration features of CPS,we extend the model based on hybrid Petri net.Taking into account the attributes of time,we add time constrains.In order to enhance the description ability of hybrid Petri net,we introduce the concept of inhibitor arcs and test arcs.Therefore we propose the concept of extended hybrid Petri net and explain how to model for CPS.Secondly,for two different scenarios of unmanned vehicle systems in CPS applications,we use the extended hybrid Petri net model and analyze the system through simulation and verification respectively.As for simulation,the model is first transformed into corresponding Simulink model according to certain rules,as well as the behavior and properties of system are analyzed by using Matlab.About verification,firstly,we propose an algorithm to construct the state evolution graph for EHPN model,and according to the graph,draw into the idea of bounded model checking,thereby the problem of model checking can be transformed into Satisfiability problem.Finally,we solve and analyze the model by SMT tool Z3.