Real-time Analysis And Verrification Of Real-Time Cyber Physical Systems

Cyber Physical System(CPS) is an emerging produc, it represents the next generation fo core information technology,even is called the third information revolution,shows the degree of attention. CPS is to pay attention to the highly centralized communication technology’s research between the real world and the virtual computation. It is known as the fusion system of "person-machine-thing", because its essence is the temporal and spatial control study.CPS as a time-critical system, time is an important consideration factor, one input at a time must produce valid output within a limited time. The basis of a complete CPS needs three kinds of technology:The first is the computing theory and techniques, whose main solution is the integration of technology of the virtual world and real space so as to reduce or avoid the drawbacks of the uncertainties of the physical world in the system; Second is the communication theory and technology, whose solution is to achieve the statute of the physical objects existed in the network, and to test network communication protocols in the WAN test platform; The last is sensor network technology, mainly used to perceive a physical object information, and sent to the network by wireless transmission.CPS be close to integration with the physical world in the aspect of time and space, coupled with the high complexity of the system, all of this have brought great challenges to the development of CPS. Most of the challenges are concentrated in the characteristics of the time. Taking some examples, how to separate the time during interaction of the computing systems and the physical world, and how to make the continuous-time of physical world discretation.And when the CPU’s function is becoming more and more complicated, it will lead to real-time action is not accurate, while the worst case execution time will be difficult to estimate. There are other problems how to ensure that the dependence between the virtual and the real world simultaneously. Automata theory on system modeling and analysis can analyze and solve some problems in a way, and an important criterion to measure the time characteristics of modeling method is its versatility and normative factors. The expressing ability of mode would at most affect the accuracy and simplicity. To make sure the system be correctly modeing, and to ensure its reliability, formal methods and description is essential.In this paper, the research begins on the basis of cyber physical system. Firstly, we introduce the the concept of the CPS, then analy the characteristic of time syntax, the following is the modeling time in the MARTE. We present the foundation of the time logic and the sortation. With the help of the hybrid automata theory, we analize the CPS, model CPS, and verify it. Then explored clock synchronization in the calculation of the interaction of systems and physical systems. And with the usage of the theory of model checking, using the UPPAAL tool proceed analysis of worst case execution time. Finally, we prove the system is decidable with the introduction of new kinds of automata. At last, we propose an example of A-Crossing-Road-System, and describe the requirement, then give the formal description and prove the correctness of the design of the system.