Modeling And Verification Based On Hybrid Spatial-temporal Petri Net For Cyber Physical System

Cyber-Physical System(CPS) is a kind of large and complex real-time feedback system which integrates calculation process the communication network, the physical process, sensor network and the control system. We need a comprehensive description and analysis on the model of the CPS due to the complex form of the internal communication, interaction and synergy between heterogeneous units. This depends on a good modeling method and perfect tools for simulation and validation.Petri Net is a digital representation of discrete variables and parallel system, it is a flow way of using the token to express the dynamic change of network, which is suitable to describe the computer system model of asynchronous concurrent. Classic Petri nets is relatively simple, it cannot describe the content of the system in terms of time and space. Therefore, the paper constructed Hybrid Spatial-Temporal Petri Net(HSPN), which makes it not only can describe the logic level and the time behavior of physical entities, but also to describe the change in state caused by changes of position.Bayesian network is a kind of mathematical model based on probability theory and graph theory, easy to deal with computer, suitable for CPS in decision-making and judgment mechanism. As a standard language for visual of the structure and behavior, UML has played a very important role in the real-time system. UML timing diagram can not only describe the state transition between objects, but also to show the order of interaction and the interaction time details.The complexity and reliability requirements of CPS system are much higher than the general traditional system, so it is not appropriate to use the traditional verification technology. UPPAAL is a real-time system verification tool based on timed automata, with strong simulation and verification capabilities according to the CPS system modeling and verification requirements. So we need to use UML timing diagram take the HSPN model into a TA model. Then use the model validation tools UPPAAL validate the model.This paper choose the Medical Cyber-Physical Systems(MCPS) that one of the most important research field of CPS as a model object. In the full analysis of CPS architecture constructed a reasonable MCPS architecture, and use HSPN modeling approach for MCPS.Using the data analysis ability of Bayesian network to uncertainty reasoning, this ability can be the internal diagnostic mechanism of MCPS. We can describe the typical event of MCPS by using UML timing diagram and convert it into TA modeling, which is ultimately simulated and verified by UPPAAL tools. The simulation and verification results of MCPS model show that the modeling method of HSPN ensured the requirement of CPS to the high reliability and real-time performance, at the same time it reflects the physical entity continuous changes in time and space. It proved that this is a feasible and security modeling mechanism, it is a very effective method for description and analysis of MCPS.