Guangdong University of Technology, Guangzhou, China

---

Abstract—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.

Index Terms—Aspect-oriented,, Cyber Physical Systems, Formal Method, ZimOO,Timed-CSP

[PDF]

Cite: Lichen Zhang, "Aspect-Oriented Formal Techniques of Cyber Physical Systems," Journal of Software vol. 7, no. 4, pp. 823-834, 2012.