Research and Implementation of Safety Verification of Polynomial Hybrid Systems Based on Symbolic-Numeric Method

Abstract:

As a mathematical model for cyber-physical system, hybrid systems are dynamical systems that are governed by interacting discrete and continuous dynamics. In this paper, we present a symbolic-numeric hybrid method to generate inequality inductive invariants for safety verification of polynomial hybrid systems, and based on this method, we develop an automated verification tool HSProver.

• Periodical: Advanced Materials Research (Volume 940)
• Pages: 485-490
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.940.485
• Online since: June 2014
• Authors: Yi Jun Zhu
• Keywords: Hybrid Systems, Invariant Generation, Safety Verification, Symbolic-Numeric Hybrid Method

References

[1] T.A. Henzinger. The theory of hybrid automata[C]. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pages 278–292. IEEE Computer Society, (1996).

DOI: 10.1109/lics.1996.561342

[2] Edward A Lee. Cyber physical systems: Design challenges[C]. In 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing (ISORC), pages 363–369. IEEE, (2008).

DOI: 10.1109/isorc.2008.25

[3] Glenford J Myers, Corey Sandler, and Tom Badgett. The art of software testing[M]. John Wiley & Sons, (2011).

DOI: 10.1002/stvr.322

[4] Doron Peled. Software reliability methods[M]. Springer, (2001).

[5] Thomas A Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: A model checker for hybrid systems[C]. In Proceedings of the International Conference on Computer Aided Verification, pages 460–463. Springer, (1997).

DOI: 10.1007/3-540-63166-6_48

[6] Goran Frehse. PHAVer: Algorithmic verification of hybrid systems past HyTech[C]. In Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control, HSCC '05, pages 258–273. Springer, (2005).

DOI: 10.1007/978-3-540-31954-2_17

[7] Goran Frehse, Colas Le Guernic, Alexandre Donze, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. SpaceEx: Scalable verification of hybrid systems[C]. In Proceedings of the International Conference on Computer Aided Verification, pages 379–395. Springer, (2011).

DOI: 10.1007/978-3-642-22110-1_30

[8] Eugene Asarin, Thao Dang, and Oded Maler. The d/dt tool for verification of hybrid systems[C]. In Proceedings of the International Conference on Computer Aided Verification, pages 365–370. Springer, (2002).

DOI: 10.1007/3-540-45657-0_30

[9] Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal-a tool suite for automatic verification of real-time systems[J]. Hybrid Systems III, pages 232–243, (1996).

DOI: 10.1007/bfb0020949

[10] Andre Platzer and Jan-David Quesel. KeYmaera: A hybrid theorem prover for hybrid systems (system description) [C]. In Automated Reasoning, pages 171–178. Springer, (2008).

DOI: 10.1007/978-3-540-71070-7_15

[11] Wang Lin, Min Wu, Zhengfeng Yang, and Zhenbing Zeng. Exact safety verification of hybrid systems using sums-of-squares representation[J]. CIENCE CHINA Information Sciences, 56, doi: 10. 1007/s11432-013-4961-z. (2013).

DOI: 10.1007/s11432-013-4961-z

[12] Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Constructing invariants for hybrid systems[J]. Formal Methods in System Design, 32: 25–55, (2008).

DOI: 10.1007/s10703-007-0046-1