Using run-time checking to provide safety and progress for distributed cyber-physical systems

Stanley Bak, Fardin Abdi Taghi Abad, Zhenqi Huang, Marco Caccamo

Research output: Contribution to conferencePaper

Abstract

Cyber-physical systems (CPS) may interact and manipulate objects in the physical world, and therefore ideally would have formal guarantees about their behavior. Performing static-time proofs of safety invariants, however, may be intractable for systems with distributed physical-world interactions. This is further complicated when realistic communication models are considered, for which there may not be bounds on message delays, or even that messages will eventually reach their destination. In this work, we address the challenge of proving safety and progress in distributed CPS communicating over an unreliable communication layer. This is done in two parts. First, we show that system safety can be verified by partially relying upon run-time checks, and that dropping messages if the run-time checks fail will maintain safety. Second, we use a notion of compatible action chains to guarantee system progress, despite unbounded message delays. We demonstrate the effectiveness of our approach on a multi-agent vehicle flocking system, and show that the overhead of the proposed run-time checks is not overbearing.

Original languageEnglish (US)
Pages287-296
Number of pages10
DOIs
StatePublished - Jan 1 2013
Event2013 IEEE 19th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2013 - Taipei, Taiwan, Province of China
Duration: Aug 19 2013Aug 21 2013

Other

Other2013 IEEE 19th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2013
CountryTaiwan, Province of China
CityTaipei
Period8/19/138/21/13

    Fingerprint

ASJC Scopus subject areas

  • Computer Science Applications
  • Software

Cite this

Bak, S., Abad, F. A. T., Huang, Z., & Caccamo, M. (2013). Using run-time checking to provide safety and progress for distributed cyber-physical systems. 287-296. Paper presented at 2013 IEEE 19th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2013, Taipei, Taiwan, Province of China. https://doi.org/10.1109/RTCSA.2013.6732229