Research On Modeling And Verification Of CPS Based On Spatial-temporal Petri Net

CPS is multidimensional complex system fused with computing system, physicalenvironment and network environment. Through3C operation, integration and depth ofcollaboration, CPS control precisely physical entities to in the physical environment,achieving real-time sensing and dynamic control of the physical environment. CPS is anintegration of computing, communication and control, which is more reliable, efficientthan traditional embedded systems, and has a stronger collaborative computingprocessing power. CPS has a wide range of application prospects, which is thedevelopment direction of future embedded systems.However, CPS not only has the advantages above, but also faces enormouschallenges. Since CPS is a kind of large, heterogeneous, distributed and real-timefeedback system which is integrated with multiple heterogeneous subsystem via thenetwork, its system complexity is above the general information system. CPS introduceda control system for changing physical environment, which brings tremendous difficultiesto development as well as its system complexity. Looking for an appropriatemethodology for developing CPS is one of the most important research directions aboutCPS.Timed Petri nets is an important formal tool for modeling and analyzing distributed,parallel, and real-time systems, which provide a solid foundation for modeling CPS.However, Timed Petri net lacks of the ability of describing spatial information, so it can’tmodel CPS totally. So the main objective of this paper is to expand Timed Petri net foreliminating the defect, make it possible to descript the position changes of the physicalentities. The main contents as follows: first, we conduct a detailed analysis of thecharacteristics of CPS’s physical layer, and learn CPS’s physical entities’ properties andtheir location changes process in-depth form two aspects of their classification andfeature; In the second, by analyzing the characteristics that Spatial-Temporal Petri net must meet, we introduce space factor into the traditional Timed Petri net, then we get theformal definition of the Spatial-Temporal Petri net. Spatial-Temporal Petri net (STPN)can not only describe logical and time-level the behavior of physical entities, but also thechange of state caused by the position change of the physical entities; At last, byregarding model checking technology as the core idea we will present a theoreticalapproach to verify behavior property, data-related property, and time-related property ofSpatial-Temporal Petri net model.In-depth study of CPS physical entities’ modeling and verification method can notonly improve the credibility of the CPS effectively, but also promote its popularity ofapplication.