An efficient framework for barrier certificate generation of uncertain nonlinear

被引:12
作者
Yang, Zhengfeng [1 ]
Wu, Min [1 ]
Lin, Wang [2 ,3 ]
机构
[1] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China
[2] Zhejiang Sci Tech Univ, Sch Informat Sci & Technol, Hangzhou 310018, Zhejiang, Peoples R China
[3] Nanjing Univ, State Key Lab Novel Software Technol, Nanjing 210023, Jiangsu, Peoples R China
基金
中国国家自然科学基金;
关键词
Formal verification; Uncertain hybrid systems; Barrier certificates; Sum of squares programming; Interval verification; SYSTEMS; STABILITY;
D O I
10.1016/j.nahs.2019.100837
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Due to the ability to handle uncertain nonlinear hybrid systems, barrier certificate based method has been widely used in safety verification problem. In this paper, an efficient framework, combining sum of squares programming with interval analysis, is proposed to generate barrier certificates for uncertain nonlinear hybrid systems. It utilizes the feature of bounded uncertainties to get a deterministic hybrid system, whose barrier certificates can be efficiently computed using sum of squares programming. The computed barrier certificates are then chosen as candidate barrier certificates for the original uncertain hybrid system, and need to be checked the satisfaction of the associated barrier certificate conditions, via an interval analysis based method. As an application, our approach is used to verify safety properties of non-polynomial hybrid systems. Some experimental results are given to show the efficiency of our approach. (c) 2019 Published by Elsevier Ltd.
引用
收藏
页数:17
相关论文
共 33 条
[1]  
Alefeld G., 1983, Introduction to Interval Computations
[2]   THE ALGORITHMIC ANALYSIS OF HYBRID SYSTEMS [J].
ALUR, R ;
COURCOUBETIS, C ;
HALBWACHS, N ;
HENZINGER, TA ;
HO, PH ;
NICOLLIN, X ;
OLIVERO, A ;
SIFAKIS, J ;
YOVINE, S .
THEORETICAL COMPUTER SCIENCE, 1995, 138 (01) :3-34
[3]  
[Anonymous], ARXIV150104578
[4]   Stability and robustness analysis of nonlinear systems via contraction metrics and SOS programming [J].
Aylward, Erin M. ;
Parrilo, Pablo A. ;
Slotine, Jean-Jacques E. .
AUTOMATICA, 2008, 44 (08) :2163-2170
[5]  
Bouissou O, 2014, IEEE DECIS CONTR P, P753, DOI 10.1109/CDC.2014.7039472
[6]  
Chen CL, 2016, PROCEEDINGS OF 2016 INTERNATIONAL CONFERENCE ON APPLIED SYSTEM INNOVATION (ICASI)
[7]   Existence of solutions to systems of underdetermined equations and spherical designs [J].
Chen, Xiaojun ;
Womersley, Robert S. .
SIAM JOURNAL ON NUMERICAL ANALYSIS, 2006, 44 (06) :2326-2341
[8]   Taylor Model Flowpipe Construction for Non-linear Hybrid Systems [J].
Chen, Xin ;
Abraham, Erika ;
Sankaranarayanan, Sriram .
PROCEEDINGS OF THE 2012 IEEE 33RD REAL-TIME SYSTEMS SYMPOSIUM (RTSS), 2012, :183-192
[9]   Estimating the domain of attraction for non-polynomial systems via LMI optimizations [J].
Chesi, Graziano .
AUTOMATICA, 2009, 45 (06) :1536-1541
[10]  
Coste M., 1998, REAL ALGEBRAIC GEOME, V36