Aspect-Oriented Formal Techniques of Cyber Physical Systems

摘要

Cyber-physical systems pose considerable technical challenges, ranging from the distributed programming paradigms to networking protocols with timeliness as a structuring concern, including systems theory that combines physical concerns and computational concerns. Formal specification techniques for such systems have to be able to describe all these concerns. Unfortunately, a single specification technique that is well suited for all these concerns s is yet not available. Instead one finds various specialized techniques that are very good at describing individual concerns of cyber-physical system. This observation has led to research into the combination and semantic integration of specification techniques. This paper proposes a formwork for specifying cyber physical systems based on aspect-oriented formal method, which exploits the diversity and power of existing formal specification languages. There is no requirement that different aspects of a system should be expressed in the same language. So the different aspects can be specified by one formal specification technique or different formal specification techniques. The proposed aspect-oriented formal framework is such a formwork. On the one hand, it can deal with continuous-time systems based on sets of ordinary differential equations. On the other hand, it can deal with discrete-event systems, without continuous variables or differential equations. We present a combination of the formal methods Timed-CSP, ZimOO and differential (algebraic) equations or differential logic. Each method can describe certain aspects of a cyber physical system: CSP can describe communication, concurrent and real-time requirements; ZimOO expresses complex data operations; differential (algebraic) equations model the dynamics and control (DC) parts. Two case studies illustrate the specification process of aspect-oriented formal specification for cyber physical systems.