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 条
  • [31] FORMAL VERIFICATION OF SAFETY-CRITICAL SYSTEMS
    MOSER, LE
    MELLIARSMITH, PM
    SOFTWARE-PRACTICE & EXPERIENCE, 1990, 20 (08) : 799 - 821
  • [32] Safety verification of non-linear hybrid systems is quasi-decidable
    Stefan Ratschan
    Formal Methods in System Design, 2014, 44 : 71 - 90
  • [33] TERMINATION ANALYSIS OF SAFETY VERIFICATION FOR NON-LINEAR ROBUST HYBRID SYSTEMS
    She, Zhikun
    ICINCO 2011: PROCEEDINGS OF THE 8TH INTERNATIONAL CONFERENCE ON INFORMATICS IN CONTROL, AUTOMATION AND ROBOTICS, VOL 1, 2011, : 251 - 261
  • [34] Combining Analytical Technique and Randomized Algorithm in Safety Verification of Stochastic Hybrid Systems
    Julius, A. Agung
    D'Innocenzo, Alessandro
    2014 AMERICAN CONTROL CONFERENCE (ACC), 2014,
  • [35] Safety verification of non-linear hybrid systems is quasi-decidable
    Ratschan, Stefan
    FORMAL METHODS IN SYSTEM DESIGN, 2014, 44 (01) : 71 - 90
  • [36] Verification of hybrid controlled processing systems based on decomposition and deduction
    Frehse, G
    Stursberg, O
    Engell, S
    Huuck, R
    Lukoschus, B
    PROCEEDINGS OF THE 2001 IEEE INTERNATIONAL SYMPOSIUM ON INTELLIGENT CONTROL (ISIC'01), 2001, : 150 - 155
  • [37] Safety Verification of State/Time-Driven Hybrid Systems Using Barrier Certificates
    Wang Guobin
    Liu Jing
    Sun Haiying
    Liu Jie
    Ding Zuohua
    Zhang Miaomiao
    PROCEEDINGS OF THE 35TH CHINESE CONTROL CONFERENCE 2016, 2016, : 2483 - 2489
  • [38] Safety Verification of Hybrid Systems Using Certified Multiple Lyapunov-Like Functions
    She, Zhikun
    Song, Dan
    Li, Meilun
    COMPUTER ALGEBRA IN SCIENTIFIC COMPUTING (CASC 2015), 2015, 9301 : 440 - 456
  • [39] Component-Based Modeling and Verification of Dynamic Adaptation in Safety-Critical Embedded Systems
    Adler, Rasmus
    Schaefer, Ina
    Trapp, Mario
    Poetzsch-Heffter, Arnd
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2010, 10 (02)
  • [40] Span-reachability and observability of bilinear hybrid systems
    Petreczky, Mihaly
    van Schuppen, Jan H.
    AUTOMATICA, 2010, 46 (03) : 501 - 509
12345