Earticle

초록

영어

Transportation cyber physical systems such as automotive, aviation, and rail involve interactions between software controllers, communication networks, and physical devices. These systems are among the most complex cyber physical systems being designed by humans, but added time and cost constraints make their development a significant technical challenge. Formal specification technologies are now indispensable for quickly developing safe and reliable transportation systems. In this paper, we propose a formal specification approach for Transportation cyber physical systems. The proposed 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 dynamic logic (DL). Each method can describe certain aspects of a transportation cyber physical system: CSP can describe communication, concurrent and real-time requirements; ZimOO expresses complex data operations; differential dynamic logic (DL) model the dynamics and control (DC) parts. A case study of train control system illustrates the specification process for Transportation cyber physical systems.

목차

Abstract
 1. Introduction
 2. Formal Specification for Transportation Cyber Physical Systems
 3. Case Study: Formal Specification of Train Control Systems
 4. Conclusion
 Acknowledgements
 References

키워드

저자

• Lichen Zhang [ Shanghai Key Laboratory of Trustworthy Computing East China Normal University, Shanghai 200062, China ] Corresponding author
• Jifeng He [ Shanghai Key Laboratory of Trustworthy Computing East China Normal University, Shanghai 200062, China ]
• Wensheng Yu [ Shanghai Key Laboratory of Trustworthy Computing East China Normal University, Shanghai 200062, China ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Multimedia and Ubiquitous Engineering

• 간기

  월간

• pISSN

  1975-0080

• 수록기간

  2008~2016

• 등재여부

  SCOPUS

• 십진분류

  KDC 505 DDC 605