TY - GEN
T1 - Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems
AU - Tran, Hoang Dung
AU - Nguyen, Luan Viet
AU - Musau, Patrick
AU - Xiang, Weiming
AU - Johnson, Taylor T.
N1 - Funding Information:
Acknowledgments. The material presented in this paper is based upon work supported by the Air Force Office of Scientific Research (AFOSR) through contract number FA9550-18-1-0122 and the Defense Advanced Research Projects Agency (DARPA) through contract number FA8750-18-C-0089. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of AFOSR or DARPA.
Publisher Copyright:
© 2019, IFIP International Federation for Information Processing.
PY - 2019
Y1 - 2019
N2 - Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent transportation, where autonomous vehicles communicate and cooperate with each other via a high-speed communication network. Such systems require an ability to identify maneuvers in real-time that cause dangerous circumstances and ensure the implementation always meets safety-critical requirements. In this paper, we propose a real-time decentralized safety verification approach for a distributed multi-agent CPS with the underlying assumption that all agents are time-synchronized with a low degree of error. In the proposed approach, each agent periodically computes its local reachable set and exchanges this reachable set with the other agents with the goal of verifying the system safety. Our method, implemented in Java, takes advantages of the timing information and the reachable set information that are available in the exchanged messages to reason about the safety of the whole system in a decentralized manner. Any particular agent can also perform local safety verification tasks based on their local clocks by analyzing the messages it receives. We applied the proposed method to verify, in real-time, the safety properties of a group of quadcopters performing a distributed search mission.
AB - Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent transportation, where autonomous vehicles communicate and cooperate with each other via a high-speed communication network. Such systems require an ability to identify maneuvers in real-time that cause dangerous circumstances and ensure the implementation always meets safety-critical requirements. In this paper, we propose a real-time decentralized safety verification approach for a distributed multi-agent CPS with the underlying assumption that all agents are time-synchronized with a low degree of error. In the proposed approach, each agent periodically computes its local reachable set and exchanges this reachable set with the other agents with the goal of verifying the system safety. Our method, implemented in Java, takes advantages of the timing information and the reachable set information that are available in the exchanged messages to reason about the safety of the whole system in a decentralized manner. Any particular agent can also perform local safety verification tasks based on their local clocks by analyzing the messages it receives. We applied the proposed method to verify, in real-time, the safety properties of a group of quadcopters performing a distributed search mission.
UR - http://www.scopus.com/inward/record.url?scp=85067344101&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85067344101&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-21759-4_15
DO - 10.1007/978-3-030-21759-4_15
M3 - Conference contribution
AN - SCOPUS:85067344101
SN - 9783030217587
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 261
EP - 277
BT - Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings
A2 - Pérez, Jorge A.
A2 - Yoshida, Nobuko
PB - Springer Verlag
T2 - 39th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019
Y2 - 17 June 2019 through 21 June 2019
ER -