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

To solve the lack of scattered crosscutting concerns in object-oriented systems, the aspect-oriented programming was proposed. With the development of aspect-oriented programming technology, AOP ideas are no longer limited to programming, but beginning to affect all stages of software development. And aspect-oriented software development techniques formed. Aspect-oriented modeling is a consistent method to describe, structure, records and visual aspect-oriented design, and is an effective measure for Aspect-oriented software development. But still have few aspect-oriented formal method applied research so far. It is difficult to use the rigorous mathematical logic to express and demonstrates the correctness of the software design process in the use process.With the development of the cloud computing and computer network technology, Real-time system application and design technology become computer science research hotspot. Especially the design concept of Cyber Physical network was proposed, it makes application of real-time system integrated computer and network system environment, which can be as small vehicle control systems, large to the national power grids, satellite communication systems. The whole system to research involves modeling, logic, concurrency, real-time, safety, etc. The existing technical difficulties including model design problems, management too much effort, time cycle is long, the network computing and physical systems concurrency issues have significant differences.In view of the above questions, this paper systematically introduces the characteristics of Cyber Physical network environment, extract the time characteristics from the network environment and combine with real-time system. In order to be able to very good expression real-time characteristics, this paper expand real-time aspects based on Time-CSP. This paper describes the basic concept and key ideas of aspect-oriented technology and detailed analysis of object-oriented formal languages Object-Z. This paper expanded formalized for aspect-oriented based on Object-Z and discussed aspect-oriented formalized method in the Cyber-Physical network environment. Meanwhile increase separation variable in the basic elements and crosscutting concerns the formalism description to achieve formalization aspect-oriented characteristics. In order to meet the design requirements in real-time systems the aspect-oriented formalized method are given. Through the comprehensive other scholars' research results in formalization of real-time system time characteristics and formalized extension methods based on Object-Z aspect-oriented, this paper gives a comprehensive model which can fully describe the characteristics of the real-time operation system in the Cyber-Physical network environment. Meanwhile in the design process can full use of formal languages rigorous mathematical logic to solve the process of developing the uncertainty and inconsistency problem. Finally, this paper demonstrates the correctness of the above ideas through the intelligent transportation system of the train dispatching control system.