Formal Modeling And Analysis Of Cyber Physical System

CPS is a kind of complex equipment system which integrates physical objects and calculating unit through communication network. Facing the trend of high flexibility and the complexity of function of systematic integration of physical objects, program design has become more complicated, and difficult to maintain. CPS can properly handle the defects, it is closely integrated with the physical world in time and space, real-time systems demanding very high time characteristics and the relationship between high interconnection continuous and discrete jumps event is a emerging technology that integrate the new sensor technology, intelligent control technology based on embedded system. It can realize close integration of human machine and material.For the question of single function and narrow range of application traditional real-time embedded system, CBS closely link the computation, communication and real material, which make the physical device be accurately controlled and let the whole world link. When facing the constantly changing application environment, it can change real-time state by itself so that can ensure the work safety, real-time and stability of application system.With the increasingly widespread research of CPS, including modeling language and software tools, the safety and stability of system security is the focus problem. Modelica modeling language ignores the internal difference model of each application domain. They communicate with the interface mode to realize multi-domain modeling function. It solve the shortcomings of existing domain modeling language of which development model is restricted to all kinds of application domain and also to be applied in many fields of application. Differential logic is based on the mathematical equation to describe the hybrid system, and it stipulates each system property and verify its correctness. Through the reasoning ability of automation differential logic, the logical description of various properties in the system and analyze system by the theorem of utilization and the choice, it could achieve the best system performance.This paper deeply research on hybrid system by using differential logic analysis method, and combined with automatic train control system, analyses the established system model by differential logic method, also alidade the security and stability of the real-time system. Firstly, the paper abstract and separate the control system to time model, communication model, physical model and other aspects, stipulate property and describe modeling, and then mix together the model into the control system structure, regularly combined into a complete control system model. Finally, test the control system through the performance of real-time reasoning to say that logic analysis method of information is reasonable and feasible to hybrid system.