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 条
  • [21] Positive Invariance of Constrained Affine Dynamics and Its Applications to Hybrid Systems and Safety Verification
    Shen, Jinglai
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2012, 57 (01) : 3 - 18
  • [22] Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants
    Sogokon, Andrew
    Jackson, Paul B.
    Johnson, Taylor T.
    JOURNAL OF AUTOMATED REASONING, 2019, 63 (04) : 1005 - 1029
  • [23] Modeling and verification of hybrid systems based on equations
    Ogata, K
    Yamagishi, D
    Seino, T
    Futatsugi, K
    DESIGN METHODS AND APPLICATIONS FOR DISTRIBUTED EMBEDDED SYSTEMS, 2004, 150 : 43 - 52
  • [24] Hybrid Tools for Hybrid Systems - Proving Stability and Safety at Once
    Moehlmann, Eike
    Hagemann, Willem
    Theel, Oliver
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2015), 2015, 9268 : 222 - 239
  • [25] Verification of Periodically Controlled Hybrid Systems: Application to an Autonomous Vehicle
    Wongpiromsarn, Tichakorn
    Mitra, Sayan
    Lamperski, Andrew
    Murray, Richard M.
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2012, 11
  • [26] Computational techniques for the verification of hybrid systems
    Tomlin, CJ
    Mitchell, I
    Bayen, AM
    Oishi, M
    PROCEEDINGS OF THE IEEE, 2003, 91 (07) : 986 - 1001
  • [27] Probabilistic Safety Verification of Stochastic Hybrid Systems Using Barrier Certificates
    Huang, Chao
    Chen, Xin
    Lin, Wang
    Yang, Zhengfeng
    Li, Xuandong
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2017, 16
  • [28] On the applicability of hybrid systems safety verification tools from the automotive perspective
    Stefan Schupp
    Erika Ábrahám
    Md Tawhid Bin Waez
    Thomas Rambow
    Zeng Qiu
    International Journal on Software Tools for Technology Transfer, 2024, 26 : 49 - 78
  • [29] Approximate Safety Verification and Control of Partially Observable Stochastic Hybrid Systems
    Lesser, Kendra
    Oishi, Meeko
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2017, 62 (01) : 81 - 96
  • [30] On the applicability of hybrid systems safety verification tools from the automotive perspective
    Schupp, Stefan
    Abraham, Erika
    Waez, Md Tawhid Bin
    Rambow, Thomas
    Qiu, Zeng
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2024, 26 (01) : 49 - 78