Aspect-Oriented Formal Verification Method For Real-Time System In Cyber Physical Systems

The real-time system based on Cyber-physical network environment is a multi-dimensional complex system which is computing, networking and physical environment. By the depth of the organic integration and collaboration of 3C (Computation, Communication, Control) technology, large-scale engineering systems achieve real-time perception, dynamic control and information services. The real-time system based on Cyber-physical network environment achieves computing, communications and integration design of physical systems, making the system more reliable, efficient, real-time collaboration. It has very important and broad application prospects. In recent years, the real-time system based on Cyber-physical network environment has not only become an important direction of research at home and abroad, but also expected to become a business priority of the industries. It is very important to carry out real-time systems based on Cyber-physical network environment.This article attempts to establish a method of aspect-oriented formal verification for real-time system based on Cyber-physical network environment. The method extends formal verification method to aspect-oriented. This paper describe aspect-oriented framework of non-functional requirements, functional interfaces and non-functional interface definition by aspect-oriented formal modeling and verification. variety of system features make verification complexity exponential explosion. in the formal verification aspect-oriented techniques can be usedA variety of features that make verification system complexity exponential effectively and decomposition of the abstractBecause the CPS and features can be expressed as a logical formula respectively, so to test whether the system meets the feature, just test the logic of the system whether contains the logic of the features; in order to test the system whether contains a side module, just verify the logic of the system whether contains the logic of the aspect model. In the third chapter, we will see an aspect-oriented approach for the establishment of VDM++ model is very effective. In the fourth chapter, we will see an application example--air traffic control voice communications systems, and verification of the system based on aspect-oriented VDM++.This paper introduces the formal verification method of the real-time system based on Cyber-physical network environment, proposes aspect-oriented framework for the non-functional requirements. Especially introduce the aspect-oriented programming into formal verification. The main tool is VDM++, and it is applied in the air traffic control voice communication system.