Formal Specification for Real Time Cyber Physical Systems Using Aspect-Oriented Approach

This paper proposes an approach for specifying real time cyber physical systems based on aspect-oriented formal specification, which exploits the diversity and power of existing formal specification languages. We provide an aspect-oriented specification approach based on the combination of Object-Z and Time-CSP. We increase separation variable in the basic elements and crosscutting concerns to achieve formalization of aspect-oriented characteristics. This paper gives a comprehensive model which can fully describe the characteristics of the real-time requirements in the cyber-physical systems. This aspect oriented formal specification method simplifies the requirement analysis process of real time cyber physical systems. A case study of a train control system illustrates the specification process of aspect-oriented formal specification for real time cyber physical systems.