Safety and progress for distributed cyber-physical systems with unreliable communication

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

Research output: Contribution to journalArticlepeer-review

Abstract

Cyber-physical systems (CPSs) may interact and manipulate objects in the physical world, and therefore formal guarantees about their behavior are strongly desired. 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 when considering that messages will eventually reach their destination. In this work, we address the challenge of proving safety and progress in distributed CPSs communicating over an unreliable communication layer. We show that for this type of communication model, system safety is closely related to the results of a hybrid system's reachability computation, which can be computed at runtime. However, since computing reachability at runtime may be computationally intensive, we provide an approach that moves significant parts of the computation to design time. This approach is demonstrated with a case study of a simulation of multiple vehicles moving within a shared environment.

Original languageEnglish (US)
Article number76
JournalACM Transactions on Embedded Computing Systems
Volume14
Issue number4
DOIs
StatePublished - Sep 1 2015

Keywords

  • Cyber-physical systems
  • Distributed system design
  • Hybrid automata
  • Reachability computation
  • Runtime verification

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Safety and progress for distributed cyber-physical systems with unreliable communication'. Together they form a unique fingerprint.

Cite this