Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
Special Issue on Distributed Hybrid Systems

Real-Time Verification for Distributed Cyber-Physical Systems

PDF
  • Hoang-Dung Tran,
  • Luan Viet Nguyen,
  • Patrick Musau,
  • Weiming Xiang,
  • Taylor T. Johnson
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
DOI: https://doi.org/10.4230/LITES.8.2.7

Published 2022-12-07

Keywords

  • Verification,
  • Reachability Analysis,
  • Distributed Cyber-Physical Systems

How to Cite

[1]
Tran, H.-D., Nguyen, L.V., Musau, P., Xiang, W. and Johnson, T.T. 2022. Real-Time Verification for Distributed Cyber-Physical Systems. Leibniz Transactions on Embedded Systems. 8, 2 (Dec. 2022), 07:1–07:19. DOI:https://doi.org/10.4230/LITES.8.2.7.

Copyright (c) 2022 Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

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.

PDF

References

  1. Matthias Althoff. An introduction to cora 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems, 2015.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  15. Alwyn E Goodloe and Lee Pike. Monitoring distributed real-time systems: A survey and future directions, 2010.
  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.
  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.
  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.
  20. Soonho Kong, Sicun Gao, Wei Chen, and Edmund Clarke. dReach: δ-Reachability Analysis for Hybrid Systems, pages 200-205. Springer, 2015.
  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.
  22. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558-565, 1978.
  23. Colas Le Guernic and Antoine Girard. Reachability analysis of hybrid systems using support functions. In Computer Aided Verification, pages 540-554. Springer, 2009.
  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.
  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.
  27. Nancy Lynch, Roberto Segala, Frits Vaandrager, and Henri B Weinberg. Hybrid i/o automata. Springer, 1996.
  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.
  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.
  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.
  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.
  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.
  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.