Modeling And Verification Of Cyber Physical Systems Based On Formal Method

The object-oriented programming technology is one of the most important contributions in software development history, which achieves abstraction, hiding information and making program modular through packaged, succesive and polymorphic system, even makes it possible for the developers develop effective and control the large complex system. it can, However, only solve the relationship in the longitudinal side, always ignores the relationship of lateral dependence, which results in the process of implementing the software system, some crosscutting concerns discrete distribution in all modules, some logical business code and lateral focus have difficults to locate clear and tangles phenomenon about code, the tangles phenomenon is the core factor that leads to the software system complicated and the complexity is uncessary. It reduces the cohesion and intelligibility of system and increases the possibility of mistaking in designing program, makes some fuctional components reused difficultly and projects unable to continue developing and maintaining.The aspect-oriented programming technology inheritates the merits of the object-oriented programming technology well and can make up for the deficiencies in the designing program which considers lateral focus. It can go deep into the internal object, can extract and model the crosscutting focus, make a good separation from the core of the system. Thus it reduces the degree of coupling between the module of system effectively, the ideology of the aspect-oriented programming was used to the analysis stage and design stage of real-time system, which can greatly improve the intelligibility and code reusability while reducing the degree of coupling between the system modules.With widely use of software applications, especially in the most advanced fields, the security and reliability of software becomes a very important issue. Formal methods to define the regulations of the hardware and software systems on the basis of the mathematics and verify the system. Its core is to construct mathematical models, as well as to analyze and verify by computing the nature of model. Formal methods provides the percise definition in the concept of compatibility, integrality and accuracy of implement, which can specify and verify the software system and its natures clearly, precisely, abstractly and concisely, thus can greatly improve the safety and reliability of the software.In this paper, we use the formal method to model CPS, combined with AOP techniques to separate CPS abstractly into three sides of information, communication and physics, adopting ZimOO to model the aspect of information, adopting CSP to model the aspect of communication, adopting the differential dynamic logic to model the aspect of physics, after the establishment of three sub-aspects models, then form a complete system model by integrating the three sub-aspects through the ideology of aspect-oriented.Finally, we descibe and validate the process of the formal modeling through an instance of the train schedluling and controlling system.