Document Open Access Logo

Real-Time Verification for Distributed Cyber-Physical Systems

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

PDF
Thumbnail PDF

File

LITES.8.2.7.pdf
  • Filesize: 1.2 MB
  • 19 pages

Document Identifiers

Author Details

Hoang-Dung Tran
  • University of Nebraska-Lincoln, Lincoln, Nebraska, USA
Luan Viet Nguyen
  • University of Dayton, Dayton, Ohio, USA
Patrick Musau
  • Vanderbilt University, Nashville, Tennessee, USA
Weiming Xiang
  • Augusta University, Nashville, Tennessee, USA
Taylor T. Johnson
  • Vanderbilt University, Nashville, Tennessee, USA

Cite AsGet BibTex

Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson. Real-Time Verification for Distributed Cyber-Physical Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 07:1-07:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LITES.8.2.7

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 reachability approach for safety verification of 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.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Distributed computing methodologies
Keywords
  • Verification
  • Reachability Analysis
  • Distributed Cyber-Physical Systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Matthias Althoff. An introduction to cora 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems, 2015. Google Scholar
  2. Karl Johan Aström, Tore Hägglund, and Karl J Astrom. Advanced PID control, volume 461. ISA-The Instrumentation, Systems, and Automation Society, 2006. Google Scholar
  3. Kyungmin Bae, Joshua Krisiloff, José Meseguer, and Peter Csaba Ölveczky. Designing and verifying distributed cyber-physical systems using multirate pals: An airplane turning control system case study. Science of Computer Programming, 103:13-50, 2015. Google Scholar
  4. Stanley Bak and Parasara Sridhar Duggirala. Hylaa: A tool for computing simulation-equivalent reachability for linear systems. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pages 173-178. ACM, 2017. Google Scholar
  5. Stanley Bak and Parasara Sridhar Duggirala. Simulation-equivalent reachability of large linear systems with inputs. In International Conference on Computer Aided Verification, pages 401-420. Springer, 2017. Google Scholar
  6. Stanley Bak, Taylor T Johnson, Marco Caccamo, and Lui Sha. Real-time reachability for verified simplex design. In Real-Time Systems Symposium (RTSS), 2014 IEEE, pages 138-148. IEEE, 2014. Google Scholar
  7. Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. Flow*: An analyzer for non-linear hybrid systems. In International Conference on Computer Aided Verification, pages 258-263. Springer, 2013. Google Scholar
  8. Xin Chen and Sriram Sankaranarayanan. Model predictive real-time monitoring of linear systems. In Real-Time Systems Symposium (RTSS), 2017 IEEE, pages 297-306. IEEE, 2017. Google Scholar
  9. Thao Dang and Oded Maler. Reachability analysis via face lifting. In Hybrid Systems: Computation and Control (HSCC '98), pages 96-109. Springer, 1998. LNCS 1386. Google Scholar
  10. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  11. Parasara Sridhar Duggirala, Taylor T Johnson, Adam Zimmerman, and Sayan Mitra. Static and dynamic analysis of timed distributed traces. In Real-Time Systems Symposium (RTSS), 2012 IEEE 33rd, pages 173-182. IEEE, 2012. Google Scholar
  12. John C Eidson, Edward A Lee, Slobodan Matic, Sanjit A Seshia, and Jia Zou. Distributed real-time software for cyber-physical systems. Proceedings of the IEEE, 100(1):45-59, 2012. Google Scholar
  13. Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. Spaceex: Scalable verification of hybrid systems. In Computer Aided Verification, pages 379-395. Springer, 2011. Google Scholar
  14. Antoine Girard, Colas Le Guernic, and Oded Maler. Efficient computation of reachable sets of linear time-invariant systems with inputs. In Hybrid Systems: Computation and Control, pages 257-271. Springer, 2006. Google Scholar
  15. Alwyn E Goodloe and Lee Pike. Monitoring distributed real-time systems: A survey and future directions, 2010. Google Scholar
  16. T. A. Henzinger. The theory of hybrid automata. In IEEE Symposium on Logic in Computer Science (LICS), page 278, Washington, DC, USA, 1996. IEEE Computer Society. Google Scholar
  17. Thomas A Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. Hytech: A model checker for hybrid systems. In Computer aided verification, pages 460-463. Springer, 1997. Google Scholar
  18. Taylor T. Johnson, Stanley Bak, Marco Caccamo, and Lui Sha. Real-time reachability for verified simplex design. ACM Trans. Embed. Comput. Syst., 15(2), February 2016. URL: https://doi.org/10.1145/2723871.
  19. Taylor T Johnson and Sayan Mitra. Parametrized verification of distributed cyber-physical systems: An aircraft landing protocol case study. In Cyber-Physical Systems (ICCPS), 2012 IEEE/ACM Third International Conference on, pages 161-170. IEEE, 2012. Google Scholar
  20. Soonho Kong, Sicun Gao, Wei Chen, and Edmund Clarke. dReach: δ-Reachability Analysis for Hybrid Systems, pages 200-205. Springer, 2015. Google Scholar
  21. Pratyush Kumar, Dip Goswami, Samarjit Chakraborty, Anuradha Annaswamy, Kai Lampka, and Lothar Thiele. A hybrid approach to cyber-physical systems verification. In Proceedings of the 49th Annual Design Automation Conference, pages 688-696. ACM, 2012. Google Scholar
  22. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558-565, 1978. Google Scholar
  23. Colas Le Guernic and Antoine Girard. Reachability analysis of hybrid systems using support functions. In Computer Aided Verification, pages 540-554. Springer, 2009. Google Scholar
  24. Yixiao Lin and Sayan Mitra. Starl: Towards a unified framework for programming, simulating and verifying distributed robotic systems. CoRR, abs/1502.06286, 2015. URL: http://arxiv.org/abs/1502.06286.
  25. Stefan B Liu, Hendrik Roehm, Christian Heinzemann, Ingo Lütkebohle, Jens Oehlerking, and Matthias Althoff. Provably safe motion of mobile robots in human environments. In Intelligent Robots and Systems (IROS), 2017 IEEE/RSJ International Conference on, pages 1351-1357. IEEE, 2017. Google Scholar
  26. Sarah M Loos, André Platzer, and Ligia Nistor. Adaptive cruise control: Hybrid, distributed, and now formally verified. In International Symposium on Formal Methods, pages 42-56. Springer, 2011. Google Scholar
  27. Nancy Lynch, Roberto Segala, Frits Vaandrager, and Henri B Weinberg. Hybrid i/o automata. Springer, 1996. Google Scholar
  28. Matthew O'Kelly, Hongrui Zheng, Dhruv Karthik, and Rahul Mangharam. F1tenth: An open-source evaluation environment for continuous control and reinforcement learning. Proceedings of Machine Learning Research, 123, 2020. Google Scholar
  29. Qinghui Tang, Sandeep KS Gupta, and Georgios Varsamopoulos. A unified methodology for scheduling in distributed cyber-physical systems. ACM Transactions on Embedded Computing Systems (TECS), 11(S2):57, 2012. Google Scholar
  30. Hoang-Dung Tran, Luan Viet Nguyen, Nathaniel Hamilton, Weiming Xiang, and Taylor T. Johnson. Reachability analysis for high-index linear differential algebraic equations (daes). In 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'19). Springer International Publishing, August 2019. Google Scholar
  31. Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson. Decentralized real-time safety verification for distributed cyber-physical systems. In Jorge A. Pérez and Nobuko Yoshida, editors, Formal Techniques for Distributed Objects, Components, and Systems (FORTE'19), pages 261-277, Cham, June 2019. Springer International Publishing. Google Scholar
  32. Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang, and Taylor T Johnson. Order-reduction abstractions for safety verification of high-dimensional linear systems. Discrete Event Dynamic Systems, 27(2):443-461, 2017. Google Scholar
  33. Yuanfang Zhang, Christopher Gill, and Chenyang Lu. Reconfigurable real-time middleware for distributed cyber-physical systems with aperiodic events. In Distributed Computing Systems, 2008. ICDCS'08. The 28th International Conference on, pages 581-588. IEEE, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact