Volume 7 Number 4 (Apr. 2012)
Home > Archive > 2012 > Volume 7 Number 4 (Apr. 2012) >
JSW 2012 Vol.7(4): 823-834 ISSN: 1796-217X
doi: 10.4304/jsw.7.4.823-834

Aspect-Oriented Formal Techniques of Cyber Physical Systems

Lichen Zhang

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.

General Information

  • ISSN: 1796-217X (Online)

  • Abbreviated Title: J. Softw.

  • Frequency:  Quarterly

  • APC: 500USD

  • DOI: 10.17706/JSW

  • Editor-in-Chief: Prof. Antanas Verikas

  • Executive Editor: Ms. Cecilia Xie

  • Abstracting/ Indexing: DBLP, EBSCO,
           CNKIGoogle Scholar, ProQuest,
           INSPEC(IET), ULRICH's Periodicals
           Directory, WorldCat, etc

  • E-mail: jsweditorialoffice@gmail.com

  • Oct 22, 2024 News!

    Vol 19, No 3 has been published with online version   [Click]

  • Jan 04, 2024 News!

    JSW will adopt Article-by-Article Work Flow

  • Apr 01, 2024 News!

    Vol 14, No 4- Vol 14, No 12 has been indexed by IET-(Inspec)     [Click]

  • Apr 01, 2024 News!

    Papers published in JSW Vol 18, No 1- Vol 18, No 6 have been indexed by DBLP   [Click]

  • Jun 12, 2024 News!

    Vol 19, No 2 has been published with online version   [Click]