Preserving safety in distributed cyber physical systems with unreliable communication channels

cyber physcial;unreliable communication channels;safety;Verification

Abdi Taghi Abad, Fardin ; Caccamo ; Marco

关键词: cyber physcial;    unreliable communication channels;    safety;    Verification;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/50655/Fardin_abdi%20taghi%20abad.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

Cyber-physical systems (CPS) may interact and manipulate objects in the physical world with the aid of communication channels. Additionally, due to their nature, most CPS are safety-critical systems where there are safety invariant that need to be preserved. The big challenge is that communication channels are unreliable meaning that there may not be bounds on message delays. this will pose a threat to the safety of system. Guaranteeing safety for these systems can be even further complicated as physical components with which these systems interact may not have accurate physical models available. In this Thesis we discuss two approaches to solve the safety problem. In the first part, we discuss a general methodology and architecture for distributed CPS design in order to increase the resiliency to communication faults. In this approach, each node exploits physical connections between nodes to estimate some of the state parameters of the remote nodes in order to detect the faults and also to maintain stability of system after fault occurrence. Finally, as a case study, a fault-resilient decentralized voltage control algorithm is presented and evaluated. In the second part of the thesis, we address the challenge of proving safety and progress in distributed CPS communicating over an unreliable commu- nication 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 un- bounded 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.