Visible to the public Using Run-Time Checking to Provide Safety and Progress for Distributed Cyber-Physical SystemsConflict Detection Enabled

TitleUsing Run-Time Checking to Provide Safety and Progress for Distributed Cyber-Physical Systems
Publication TypeConference Paper
Year of Publication2013
AuthorsStanley Bak, University of Illinois at Urbana-Champaign, Fardin Abdi, University of Illinois at Urbana-Champaign, Zhenqi Huang, University of Illinois at Urbana-Champaign, Marco Caccamo, University of Illinois at Urbana-Champaign
Conference Name2013 IEEE 19th International Conference on Embedded and Real-Time Computing Systems and Applications
Date Published08/2013
PublisherIEEE Computer Society
Conference LocationTaipei, Taiwan
KeywordsClassification of Cyber-Physical System Adversaries, NSA SoS Lablets Materials, science of security, UIUC
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 statictime 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 runtime 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.

Citation Keynode-31883

Other available formats:

Using Run-Time Checking to Provide Safety and Progress for Distributed Cyber-Physical Systems