Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems

Tran, Hoang-Dung; Nguyen, Luan Viet; Musau, Patrick; Xiang, Weiming; Johnson, Taylor T.

by Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, Taylor T. Johnson

Abstract:

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.

Reference:

Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, Taylor T. Johnson, "Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems", In Formal Techniques for Distributed Objects, Components, and Systems (FORTE'19) (Jorge A. Pérez, Nobuko Yoshida, eds.), Springer International Publishing, Cham, pp. 261–277, 2019, June.

Bibtex Entry:

@InProceedings{tran2019forte,
author="Tran, Hoang-Dung
and Nguyen, Luan Viet
and Musau, Patrick
and Xiang, Weiming
and Taylor T. Johnson",
editor="P{\'e}rez, Jorge A.
and Yoshida, Nobuko",
title="Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems",
booktitle="Formal Techniques for Distributed Objects, Components, and Systems (FORTE'19)",
year="2019",
publisher="Springer International Publishing",
address="Cham",
month="June",
pages="261--277",
abstract="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.",
isbn="978-3-030-21759-4",
pdf="research/tran2019forte.pdf",
}