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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationFormal 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
EditorsJorge A. Pérez, Nobuko Yoshida
PublisherSpringer Verlag
Pages261-277
Number of pages17
ISBN (Print)9783030217587
DOIs
StatePublished - Jan 1 2019
Externally publishedYes
Event39th 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 - Kongens Lyngby, Denmark
Duration: Jun 17 2019Jun 21 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11535 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference39th 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
CountryDenmark
CityKongens Lyngby
Period6/17/196/21/19

Fingerprint

Decentralized
Safety
Real-time
Reachable Set
High-speed Networks
Autonomous Vehicles
Security systems
Telecommunication networks
Cyber Physical System
Clocks
Communication Networks
Java
Timing
Verify
Requirements
Range of data

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Tran, H. D., Nguyen, L. V., Musau, P., Xiang, W., & Johnson, T. T. (2019). Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems. In J. A. Pérez, & N. Yoshida (Eds.), 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 (pp. 261-277). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11535 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-21759-4_15

Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems. / Tran, Hoang Dung; Nguyen, Luan Viet; Musau, Patrick; Xiang, Weiming; Johnson, Taylor T.

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. ed. / Jorge A. Pérez; Nobuko Yoshida. Springer Verlag, 2019. p. 261-277 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11535 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Tran, HD, Nguyen, LV, Musau, P, Xiang, W & Johnson, TT 2019, Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems. in JA Pérez & N Yoshida (eds), 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11535 LNCS, Springer Verlag, pp. 261-277, 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, Kongens Lyngby, Denmark, 6/17/19. https://doi.org/10.1007/978-3-030-21759-4_15
Tran HD, Nguyen LV, Musau P, Xiang W, Johnson TT. Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems. In Pérez JA, Yoshida N, editors, 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. Springer Verlag. 2019. p. 261-277. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-21759-4_15
Tran, Hoang Dung ; Nguyen, Luan Viet ; Musau, Patrick ; Xiang, Weiming ; Johnson, Taylor T. / Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems. 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. editor / Jorge A. Pérez ; Nobuko Yoshida. Springer Verlag, 2019. pp. 261-277 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{21ea03c735f74c108473f18e404879f5,
title = "Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems",
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.",
author = "Tran, {Hoang Dung} and Nguyen, {Luan Viet} and Patrick Musau and Weiming Xiang and Johnson, {Taylor T.}",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-21759-4_15",
language = "English (US)",
isbn = "9783030217587",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "261--277",
editor = "P{\'e}rez, {Jorge A.} and Nobuko Yoshida",
booktitle = "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",

}

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.

PY - 2019/1/1

Y1 - 2019/1/1

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

ER -