Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation

被引:24
|
作者
Yang, Zhengfeng [1 ]
Lin, Wang [2 ]
Wu, Min [1 ]
机构
[1] E China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China
[2] Wenzhou Univ, Coll Math & Informat Sci, Wenzhou 325035, Zhejiang, Peoples R China
基金
中国国家自然科学基金;
关键词
Algorithms; Reliability; Verification; Symbolic-numeric computation; bilinear SOS programming; nonlinear hybrid system; safety verification; invariant generation; REACHABILITY; COMPUTATION; INVARIANTS; REGION;
D O I
10.1145/2629424
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
In this article, we address the problem of safety verification of nonlinear hybrid systems. A hybrid symbolic-numeric method is presented to compute exact inequality invariants of hybrid systems efficiently. Some numerical invariants of a hybrid system can be obtained by solving a bilinear SOS programming via the PENBMI solver or iterative method, then the modified Newton refinement and rational vector recovery techniques are applied to obtain exact polynomial invariants with rational coefficients, which exactly satisfy the conditions of invariants. Experiments on some benchmarks are given to illustrate the efficiency of our algorithm.
引用
收藏
页数:19
相关论文
共 50 条
  • [1] Exact safety verification of hybrid systems using sums-of-squares representation
    Lin Wang
    Wu Min
    Yang ZhengFeng
    Zeng ZhenBing
    SCIENCE CHINA-INFORMATION SCIENCES, 2014, 57 (05) : 1 - 13
  • [2] Safety Verification of Nonlinear Hybrid Systems Based on Bilinear Programming
    Zhang, Yifan
    Yang, Zhengfeng
    Lin, Wang
    Zhu, Huibiao
    Chen, Xin
    Li, Xuandong
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2018, 37 (11) : 2768 - 2778
  • [3] Exact safety verification of hybrid systems using sums-of-squares representation
    LIN Wang
    WU Min
    YANG ZhengFeng
    ZENG ZhenBing
    Science China(Information Sciences), 2014, 57 (05) : 20 - 32
  • [4] Exact safety verification of hybrid systems using sums-of-squares representation
    Wang Lin
    Min Wu
    ZhengFeng Yang
    ZhenBing Zeng
    Science China Information Sciences, 2014, 57 : 1 - 13
  • [5] Safety verification of hybrid systems by constraint propagation-based abstraction refinement
    Ratschan, Stefan
    She, Zhikun
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2007, 6 (01) : 8
  • [6] A New Barrier Certificate for Safety Verification of Hybrid Systems
    Kong, Hui
    Song, Xiaoyu
    Han, Dong
    Gu, Ming
    Sun, Jiaguang
    COMPUTER JOURNAL, 2014, 57 (07) : 1033 - 1045
  • [7] Safety verification and reachability analysis for hybrid systems
    Gueguen, Herve
    Lefebvre, Marie-Anne
    Zaytoon, Janan
    Nasri, Othman
    ANNUAL REVIEWS IN CONTROL, 2009, 33 (01) : 25 - 36
  • [8] Measurability and Safety Verification for Stochastic Hybrid Systems
    Fraenzle, Martin
    Hahn, Ernst Moritz
    Hermanns, Holger
    Wolovick, Nicolas
    Zhang, Lijun
    HSCC 11: PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2011, : 43 - 52
  • [9] Verification of the safety and attainability of hybrid systems: State of the art
    Nasri, Othman
    Lefebvre, Marie-Anne
    Guéguen, Hervé
    Zaytoon, Junan
    Journal Europeen des Systemes Automatises, 2007, 41 (7-8): : 855 - 883
  • [10] Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters
    Kong, Hui
    Bogomolov, Sergiy
    Schilling, Christian
    Jiang, Yu
    Henzinger, Thomas A.
    PROCEEDINGS OF THE 20TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS WEEK) (HSCC' 17), 2017, : 163 - 172