Document Open Access Logo

Safety Verification of Networked Control Systems by Complex Zonotopes

Authors Arvind Adimoolam , Thao Dang

PDF
Thumbnail PDF

File

LITES.8.2.1.pdf
  • Filesize: 0.71 MB
  • 22 pages

Document Identifiers

Author Details

Arvind Adimoolam
  • Indian Institute of Technology Kanpur, Rajeev Motwani Building, Kalyanpur, Kanpur, India
Thao Dang
  • VERIMAG, CNRS/University Grenoble Alpes, Bâtiment IMAG, 700 Avenue Centrale, Grenoble, France

Cite AsGet BibTex

Arvind Adimoolam and Thao Dang. Safety Verification of Networked Control Systems by Complex Zonotopes. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 01:1-01:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LITES.8.2.1

Abstract

Networked control systems (NCS) are widely used in real world applications because of their advantages, such as remote operability and reduced installation costs. However, they are prone to various inaccuracies in execution like delays, packet dropouts, inaccurate sensing and quantization errors. To ensure safety of NCS, their models have to be verified under the consideration of aforementioned uncertainties. In this paper, we tackle the problem of verifying safety of models of NCS under uncertain sampling time, inaccurate output measurement or estimation, and unknown disturbance input. Unbounded-time safety verification requires approximation of reachable sets by invariants, whose computation involves set operations. For uncertain linear dynamics, two important set operations for invariant computation are linear transformation and Minkowski sum operations. Zonotopes have the advantage that linear transformation and Minkowski sum operations can be efficiently approximated. However, they can not encode directions of convergence of trajectories along complex eigenvectors, which is closely related to encoding invariants. Therefore, we extend zonotopes to the complex valued domain by a representation called complex zonotope, which can capture contraction along complex eigenvectors for determining invariants. We prove a related mathematical result that in case of accurate feedback sampling, a complex zonotope will represent an invariant for a stable NCS. In addition, we propose an algorithm to verify the general case based on complex zonotopes, when there is uncertainty in sampling time and in input. We demonstrate the efficiency of our algorithm on benchmark examples and compare it with a state-of-the-art verification tool.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Reliability
Keywords
  • Safety Verification
  • Networked Control System
  • Reachability Analysis
  • Complex Zonotope

Metrics

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

References

  1. Arvind Adimoolam and Thao Dang. Augmented complex zonotopes for computing invariants of affine hybrid systems. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 97-115. Springer, 2017. Google Scholar
  2. Arvind Adimoolam and Thao Dang. Template complex zonotopes for stability and invariant verification. In 2017 American Control Conference (ACC), pages 2544-2549. IEEE, 2017. Google Scholar
  3. Arvind S Adimoolam and Thao Dang. Template complex zonotopes: a new set representation for verification of hybrid systems. In 2016 International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), pages 1-2. IEEE, 2016. Google Scholar
  4. Arvind S Adimoolam and Thao Dang. Using complex zonotopes for stability verification. In 2016 American Control Conference (ACC), pages 4269-4274. IEEE, 2016. Google Scholar
  5. Santosh Arvind Adimoolam. A Calculus of Complex Zonotopes for Invariance and Stability Verification of Hybrid Systems. PhD thesis, Université Grenoble Alpes, 2018. Google Scholar
  6. Assalé Adjé, Pierre-Loïc Garoche, and Alexis Werey. Quadratic zonotopes. In Asian Symposium on Programming Languages and Systems, pages 127-145. Springer, 2015. Google Scholar
  7. Assalé Adjé, Stéphane Gaubert, and Eric Goubault. Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In European Symposium on Programming, pages 23-42. Springer, 2010. Google Scholar
  8. Mohammad Al Khatib, Antoine Girard, and Thao Dang. Stability verification of nearly periodic impulsive linear systems using reachability analysis. IFAC-PapersOnLine, 48(27):358-363, 2015. Google Scholar
  9. Xavier Allamigeon, Stéphane Gaubert, and Eric Goubault. Inferring min and max invariants using max-plus polyhedra. In International Static Analysis Symposium, pages 189-204. Springer, 2008. Google Scholar
  10. Xavier Allamigeon, Stéphane Gaubert, Eric Goubault, Sylvie Putot, and Nikolas Stott. A fast method to compute disjunctive quadratic invariants of numerical programs. ACM Transactions on Embedded Computing Systems (TECS), 16(5s):1-19, 2017. Google Scholar
  11. Xavier Allamigeon, Stéphane Gaubert, Nikolas Stott, Éric Goubault, and Sylvie Putot. A scalable algebraic method to infer quadratic invariants of switched systems. ACM Transactions on Embedded Computing Systems (TECS), 15(4):1-20, 2016. Google Scholar
  12. Matthias Althoff. Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In Proceedings of the 16th international conference on Hybrid systems: computation and control, pages 173-182, 2013. Google Scholar
  13. Rajeev Alur. Formal verification of hybrid systems. In Proceedings of the ninth ACM international conference on Embedded software, pages 273-278, 2011. Google Scholar
  14. Stephen Boyd, Stephen P Boyd, and Lieven Vandenberghe. Convex optimization. Cambridge university press, 2004. Google Scholar
  15. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 84-96, 1978. Google Scholar
  16. Jamal Daafouz, Pierre Riedinger, and Claude Iung. Stability analysis and control synthesis for switched systems: a switched lyapunov function approach. IEEE transactions on automatic control, 47(11):1883-1887, 2002. Google Scholar
  17. Lei Ding, Qing-Long Han, Eyad Sindi, et al. Distributed cooperative optimal control of dc microgrids with communication delays. IEEE Transactions on Industrial Informatics, 14(9):3924-3935, 2018. Google Scholar
  18. Mirko Fiacchini and Irinel-Constantin Morărescu. Set theory conditions for stability of linear impulsive systems. In 53rd IEEE Conference on Decision and Control, pages 1527-1532. IEEE, 2014. Google Scholar
  19. 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 Proc. 23rd International Conference on Computer Aided Verification (CAV), LNCS. Springer, 2011. Google Scholar
  20. Antoine Girard. Reachability of uncertain linear systems using zonotopes. In International Workshop on Hybrid Systems: Computation and Control, pages 291-305. Springer, 2005. Google Scholar
  21. Antoine Girard and Colas Le Guernic. Zonotope/hyperplane intersection for hybrid systems reachability analysis. In International Workshop on Hybrid Systems: Computation and Control, pages 215-228. Springer, 2008. Google Scholar
  22. Michael Grant, Stephen Boyd, and Yinyu Ye. Cvx: Matlab software for disciplined convex programming, 2009. Google Scholar
  23. Thomas Heinz, Jens Oehlerking, and Matthias Woehrle. Benchmark: Reachability on a model with holes. In ARCH@ CPSWeek, pages 31-36, 2014. Google Scholar
  24. Laurentiu Hetel, Jamal Daafouz, and Claude Iung. Lmi control design for a class of exponential uncertain systems with application to network controlled switched systems. In 2007 American Control Conference, pages 1401-1406. IEEE, 2007. Google Scholar
  25. Laurentiu Hetel, Jamal Daafouz, Sophie Tarbouriech, and Christophe Prieur. Stabilization of linear impulsive systems through a nearly-periodic reset. Nonlinear Analysis: Hybrid Systems, 7(1):4-15, 2013. Google Scholar
  26. Kyoung-Dae Kim and Panganamala R Kumar. Cyber-physical systems: A perspective at the centennial. Proceedings of the IEEE, 100(Special Centennial Issue):1287-1308, 2012. Google Scholar
  27. Alexander B Kurzhanski and Pravin Varaiya. Ellipsoidal techniques for reachability analysis. In International Workshop on Hybrid Systems: Computation and Control, pages 202-214. Springer, 2000. Google Scholar
  28. Michal Kvasnica. Minkowski addition of convex polytopes, 2005. Google Scholar
  29. Ibtissem Ben Makhlouf and Stefan Kowalewski. Networked cooperative platoon of vehicles for testing methods and verification tools. In ARCH@ CPSWeek, pages 37-42, 2014. Google Scholar
  30. Antoine Miné. The octagon abstract domain. Higher-order and symbolic computation, 19(1):31-100, 2006. Google Scholar
  31. Stefan Pettersson and Bengt Lennartson. Hybrid system stability and robustness verification using linear matrix inequalities. International Journal of Control, 75(16-17):1335-1355, 2002. Google Scholar
  32. Stephen Prajna and Ali Jadbabaie. Safety verification of hybrid systems using barrier certificates. In International Workshop on Hybrid Systems: Computation and Control, pages 477-492. Springer, 2004. Google Scholar
  33. Enric Rodríguez-Carbonell and Deepak Kapur. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Science of Computer Programming, 64(1):54-75, 2007. Google Scholar
  34. Henrik Sandberg, Saurabh Amin, and Karl Henrik Johansson. Cyberphysical security in networked control systems: An introduction to the issue. IEEE Control Systems Magazine, 35(1):20-23, 2015. Google Scholar
  35. Sriram Sankaranarayanan, Thao Dang, and Franjo Ivančić. Symbolic model checking of hybrid systems using template polyhedra. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 188-202. Springer, 2008. Google Scholar
  36. Ashish Tiwari. Generating box invariants. In International Workshop on Hybrid Systems: Computation and Control, pages 658-661. Springer, 2008. Google Scholar
  37. Yu-Long Wang and Qing-Long Han. Network-based modelling and dynamic output feedback control for unmanned marine vehicles in network environments. Automatica, 91:43-53, 2018. Google Scholar
  38. Xian-Ming Zhang and Qing-Long Han. Network-based h∞ filtering using a logic jumping-like trigger. Automatica, 49(5):1428-1435, 2013. 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