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
来源：
ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS | 2015年 / 14卷 / 01期
基金：
中国国家自然科学基金;
关键词：
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 条
  • [41] Safety Enforcement for the Verification of Autonomous Systems
    de Niz, Dionisio
    Andersson, Bjorn
    Moreno, Gabriel
    AUTONOMOUS SYSTEMS: SENSORS, VEHICLES, SECURITY, AND THE INTERNET OF EVERYTHING, 2018, 10643
  • [42] Verification Condition Generation for Hybrid Systems
    Li, Xian
    Schneider, Klaus
    2015 ACM/IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CODESIGN (MEMOCODE), 2015, : 238 - 247
  • [43] Current Challenges in the Verification of Hybrid Systems
    Schupp, Stefan
    Abraham, Erika
    Chen, Xin
    Ben Makhlouf, Ibtissem
    Frehse, Goran
    Sankaranarayanan, Sriram
    Kowalewski, Stefan
    CYBER PHYSICAL SYSTEMS: DESIGN, MODELING, AND EVALUATION, CYPHY 2015, 2015, 9361 : 8 - 24
  • [44] Falsification of LTL Safety Properties in Hybrid Systems
    Plaku, Erion
    Kavraki, Lydia E.
    Vardi, Moshe Y.
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2009, 5505 : 368 - 382
  • [45] Learning Robust Embedding Representation With Hybrid Loss for Classification and Verification
    Huang, Haozhi
    Liang, Yanyan
    IEEE ACCESS, 2019, 7 : 13643 - 13652
  • [46] Safety Functions and Software Verification of NPP Safety Important Systems
    Jharko, Elena Ph.
    IFAC PAPERSONLINE, 2019, 52 (13): : 1385 - 1390
  • [47] Verification and validation of knowledge-based systems
    Tsai, WT
    Vishnuvajjala, R
    Zhang, D
    IEEE TRANSACTIONS ON KNOWLEDGE AND DATA ENGINEERING, 1999, 11 (01) : 202 - 212
  • [48] Safety Design and Verification in Reconfigurable Assembly Systems
    Mahjoub, Yassine Idel
    Berger, Thierry
    Bonte, Therese
    Sallez, Yves
    12TH INTERNATIONAL WORKSHOP ON SERVICE ORIENTED, HOLONIC AND MULTI-AGENT MANUFACTURING SYSTEMS FOR INDUSTRY OF THE FUTURE, SOHOMA 2022, 2023, 1083 : 423 - 433
  • [49] A Dissipativity Approach to Safety Verification for Interconnected Systems
    Coogan, Samuel
    Arcak, Murat
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2015, 60 (06) : 1722 - 1727
  • [50] Systems Safety Verification By Boundary Variation Analysis
    Li Wang
    Yu Wensheng
    2015 34TH CHINESE CONTROL CONFERENCE (CCC), 2015, : 2979 - 2982
12345