A Heuristical Method for Safety Verification of Nonlinear Continuous Systems
详细信息 查看官网全文
- 英文论文题名：A Heuristical Method for Safety Verification of Nonlinear Continuous Systems
- 论文作者：Wang Li ; Lu Yang ; Wensheng Yu
- 英文论文作者：Wang Li ; Lu Yang ; Wensheng Yu ; School of Computer Science ; Zhaoqing University ; Chengdu Institute of computer application ; Chinese Academy of Sciences ; School of Electronic Engineering ; Beijing University of Posts and Telecommunications
- 年：2017
- 作者机构：School of Computer Science,Zhaoqing University;Chengdu Institute of computer application,Chinese Academy of Sciences;School of Electronic Engineering,Beijing University of Posts and Telecommunications;
- 英文论文关键词：System Safety Verification ; Barrier Function ; Reachability Analysis
- 会议召开时间：2017-07-26
- 会议录名称：第36届中国控制会议论文集（B）
- 英文会议录名称：Proceedings of the 36th Chinese Control Conference（B）
- 语种：英文
- 分类号：O175
- 学会代码：KZLL
- 会议名称：第36届中国控制会议
- 会议地点：中国辽宁大连
- 主办单位：中国自动化学会控制理论专业委员会
- 学会名称：中国自动化学会控制理论专业委员会
- 页数：6
- 文件大小：478k
- 原文格式：D
- 会议级别：全国
摘要
Hybrid system is an important mathematical model for Cyber-Physical System, many physical process always modeled by differential equations. The safety verification of those systems become an urgent problem. In this paper we proposed a heuristical method to determine the system defined by nonlinear differential equation is whether safe or not, we consider the Van der Pol equation as a case study to illustrate this method. Moreover, we consider the problem of searching the barrier functions when the corresponding un-safety region enlarge, we figure out when the radius of the un-safety region is 1.2082 the system is safe. on the other side, from the point of reachablity analysis, we proved when the radius of the un-safety region enlarge to 1.209,the system become unsafe. By using this method, we consider the safety verification problem with specified precision with the radius of the unsafe region.
Hybrid system is an important mathematical model for Cyber-Physical System, many physical process always modeled by differential equations. The safety verification of those systems become an urgent problem. In this paper we proposed a heuristical method to determine the system defined by nonlinear differential equation is whether safe or not, we consider the Van der Pol equation as a case study to illustrate this method. Moreover, we consider the problem of searching the barrier functions when the corresponding un-safety region enlarge, we figure out when the radius of the un-safety region is 1.2082 the system is safe. on the other side, from the point of reachablity analysis, we proved when the radius of the un-safety region enlarge to 1.209,the system become unsafe. By using this method, we consider the safety verification problem with specified precision with the radius of the unsafe region.
Hybrid system is an important mathematical model for Cyber-Physical System, many physical process always modeled by differential equations. The safety verification of those systems become an urgent problem. In this paper we proposed a heuristical method to determine the system defined by nonlinear differential equation is whether safe or not, we consider the Van der Pol equation as a case study to illustrate this method. Moreover, we consider the problem of searching the barrier functions when the corresponding un-safety region enlarge, we figure out when the radius of the un-safety region is 1.2082 the system is safe. on the other side, from the point of reachablity analysis, we proved when the radius of the un-safety region enlarge to 1.209,the system become unsafe. By using this method, we consider the safety verification problem with specified precision with the radius of the unsafe region.
引文
[1]Hu J,Prandini M,Sastry S.Probabilistic safety analysis in three dimensional aircraft flight,Proc.IEEE Conf.Decision and Control,2003,5335-5340
[2]Tomlin C,Mitchell I,Bayen A,Oishi M.Computational techniques for the verification of hybrid systems,Proc.IEEE,2003,91(7),986-1001
[3]Glavaski S,Papachristodoulou A,Ariyur K.Safety verification of controlled advanced life support system using barrier certificates,Hybrid Systems:Computation and Control,LNCS 3414.Heidelberg,Germany:Springer-Verlag,2005,306-321
[4]Kesten Y,Pnueli A,Sifakis J,Yovine S.Integration graphs:a class of decidable hybrid systems.Hybrid systems,Springer,1993,179-208
[5]Alur R,Courcoubetis C,Halbwachs N,Henzinger T,Ho P,Nicollin X,Olivero A,Sifakis J,Yovine S.The algorithmic analysis of hybrid systems.Theoretical Computer Science,1995,138(1):3-34
[6]Henzinger T,Kopke P,Puri A,Varaiya P.What’s decidable about hybrid automata?Proceedings of the 27th annual ACM symposium on Theory of computing,ACM,1995,373-382
[7]Anai H,Weispfenning V,Reach set computations using real quantifier elimination,Hybrid Systems:Computation and Control,LNCS 2034,Heidelberg,Germany:Springer-Verlag,2001,63-76
[8]Lafferriere G,Pappas G,Yovine S.Symbolic reachability computations for families of linear vectorfields,J.Symb.Comput.,2001,32(3):231-253
[9]Botchkarev O,Tripakis S,Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations,Hy-brid Systems:Computation and Control,LNCS 1790.Heidelberg,Germany:Springer-Verlag,2000,73-88
[10]Yazarel H,Pappas J,Geometric programming relaxations for linear systems reachability,Proc.Amer.Control Conf,2004,553-559
[11]Tomlin C,Mitchell I,Bayen A,Oishi M.Computational techniques for the verification of hybrid systems.Proceedings of the IEEE,2003,91(7):986-1001
[12]Yang L,Zhan N,Xia B,Zhou C.Program verification by using DISCOVERER.Verified Software:Theories,Tools,Experiments,Springer,2008,528-538.
[13]Yang L,Zhou C,Zhan N,Xia B.Recent advances in program verification through computer algebra.Frontiers of Computer Science in China,2010,4(1):1-16
[14]Yang Z,Lin W,Wu M,Exact verification of hybrid systems based on bilinear SOS representation.To appear in ACM Transactions on Embedded Computing Systems,2014
[15]Lin W,Wu M,Yang Z,Zeng Z,Exact safety verification of hybrid systems using sums-of-squares representation.Science China Information Sciences 2014,57(5):1-13
[16]Lafferriere G,Pappas G,Sastry S.O-minimal hybrid systems.Mathematics of control,signals and systems,2000,13(1):1-21
[17]Sturm T,Tiwari A.Verification and synthesis using real quantifier elimination.Proceedings of the International Symposium on Symbolic and Algebraic Computation,ISSAC,ACM Press,2011,329-336.
[18]Tiwari A,Khanna G.Nonlinear systems:Approximating reach sets.Proceedings of the 7th International Workshop on Hybrid Systems:Computation and Control,HSCC’04,Springer,2004,600-614
[19]Sankaranarayanan S,Sipma H,Manna Z.Constructing invariants for hybrid systems.Formal Methods in System Design,2008,32:25-55
[20]Sankaranarayanan S.Automatic invariant generation for hybrid systems using ideal fixed points.Proceedings of the 13th ACM international conference on Hybrid systems:computation and control,ACM,2010,221-230.
[21]Liu J,Zhan N,Zhao H.Computing semi-algebraic invariants for polynomial dynamical systems.Proceedings of the International Conference on Embedded Software(EMSOFT),ACM,2011,97-106
[22]Ratschan S,She Z.Safety verification of hybrid systems by constraint propagation-based abstraction refinement.ACM Transactions in Embedded Computing Systems,2007,6(1):573-589
[23]Chutinan A,Krogh B.Computational techniques for hybrid system verification.IEEE Transactions on Automatic Control,2003,48(1):64-75
[24]Rodr′?guez E,Tiwari A.Generating polynomial invariants for hybrid systems.Proceedings of the 8th International Workshop on Hybrid Systems:Computation and Control,HSCC’05,Springer,2005,590-605
[25]Tiwari A,Khanna G.Nonlinear systems:Approximating reach sets.Proceedings of the 7th International Workshop on Hybrid Systems:Computation and Control,HSCC’04,Springer,2004,600-614.
[26]Ratschan S,She Z.Safety verification of hybrid systems by constraint propagation-based abstraction refinement.ACM Transactions in Embedded Computing Systems,2007,6(1):573-589
[27]Prajna S,Jadbabaie A,Pappas G.A framework for worstcase and stochastic safety verification using barrier certificates.IEEE T Automat Contr,2007.52(8):1415-1429.
[28]Khalil,Hassan K.Nonlinear systems.Macmillan Publishing Company,New York,1992.
[29]Wang G,Ordinary Differential Equation,Higher Education Press,Bei Jing,2005
[2]Tomlin C,Mitchell I,Bayen A,Oishi M.Computational techniques for the verification of hybrid systems,Proc.IEEE,2003,91(7),986-1001
[3]Glavaski S,Papachristodoulou A,Ariyur K.Safety verification of controlled advanced life support system using barrier certificates,Hybrid Systems:Computation and Control,LNCS 3414.Heidelberg,Germany:Springer-Verlag,2005,306-321
[4]Kesten Y,Pnueli A,Sifakis J,Yovine S.Integration graphs:a class of decidable hybrid systems.Hybrid systems,Springer,1993,179-208
[5]Alur R,Courcoubetis C,Halbwachs N,Henzinger T,Ho P,Nicollin X,Olivero A,Sifakis J,Yovine S.The algorithmic analysis of hybrid systems.Theoretical Computer Science,1995,138(1):3-34
[6]Henzinger T,Kopke P,Puri A,Varaiya P.What’s decidable about hybrid automata?Proceedings of the 27th annual ACM symposium on Theory of computing,ACM,1995,373-382
[7]Anai H,Weispfenning V,Reach set computations using real quantifier elimination,Hybrid Systems:Computation and Control,LNCS 2034,Heidelberg,Germany:Springer-Verlag,2001,63-76
[8]Lafferriere G,Pappas G,Yovine S.Symbolic reachability computations for families of linear vectorfields,J.Symb.Comput.,2001,32(3):231-253
[9]Botchkarev O,Tripakis S,Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations,Hy-brid Systems:Computation and Control,LNCS 1790.Heidelberg,Germany:Springer-Verlag,2000,73-88
[10]Yazarel H,Pappas J,Geometric programming relaxations for linear systems reachability,Proc.Amer.Control Conf,2004,553-559
[11]Tomlin C,Mitchell I,Bayen A,Oishi M.Computational techniques for the verification of hybrid systems.Proceedings of the IEEE,2003,91(7):986-1001
[12]Yang L,Zhan N,Xia B,Zhou C.Program verification by using DISCOVERER.Verified Software:Theories,Tools,Experiments,Springer,2008,528-538.
[13]Yang L,Zhou C,Zhan N,Xia B.Recent advances in program verification through computer algebra.Frontiers of Computer Science in China,2010,4(1):1-16
[14]Yang Z,Lin W,Wu M,Exact verification of hybrid systems based on bilinear SOS representation.To appear in ACM Transactions on Embedded Computing Systems,2014
[15]Lin W,Wu M,Yang Z,Zeng Z,Exact safety verification of hybrid systems using sums-of-squares representation.Science China Information Sciences 2014,57(5):1-13
[16]Lafferriere G,Pappas G,Sastry S.O-minimal hybrid systems.Mathematics of control,signals and systems,2000,13(1):1-21
[17]Sturm T,Tiwari A.Verification and synthesis using real quantifier elimination.Proceedings of the International Symposium on Symbolic and Algebraic Computation,ISSAC,ACM Press,2011,329-336.
[18]Tiwari A,Khanna G.Nonlinear systems:Approximating reach sets.Proceedings of the 7th International Workshop on Hybrid Systems:Computation and Control,HSCC’04,Springer,2004,600-614
[19]Sankaranarayanan S,Sipma H,Manna Z.Constructing invariants for hybrid systems.Formal Methods in System Design,2008,32:25-55
[20]Sankaranarayanan S.Automatic invariant generation for hybrid systems using ideal fixed points.Proceedings of the 13th ACM international conference on Hybrid systems:computation and control,ACM,2010,221-230.
[21]Liu J,Zhan N,Zhao H.Computing semi-algebraic invariants for polynomial dynamical systems.Proceedings of the International Conference on Embedded Software(EMSOFT),ACM,2011,97-106
[22]Ratschan S,She Z.Safety verification of hybrid systems by constraint propagation-based abstraction refinement.ACM Transactions in Embedded Computing Systems,2007,6(1):573-589
[23]Chutinan A,Krogh B.Computational techniques for hybrid system verification.IEEE Transactions on Automatic Control,2003,48(1):64-75
[24]Rodr′?guez E,Tiwari A.Generating polynomial invariants for hybrid systems.Proceedings of the 8th International Workshop on Hybrid Systems:Computation and Control,HSCC’05,Springer,2005,590-605
[25]Tiwari A,Khanna G.Nonlinear systems:Approximating reach sets.Proceedings of the 7th International Workshop on Hybrid Systems:Computation and Control,HSCC’04,Springer,2004,600-614.
[26]Ratschan S,She Z.Safety verification of hybrid systems by constraint propagation-based abstraction refinement.ACM Transactions in Embedded Computing Systems,2007,6(1):573-589
[27]Prajna S,Jadbabaie A,Pappas G.A framework for worstcase and stochastic safety verification using barrier certificates.IEEE T Automat Contr,2007.52(8):1415-1429.
[28]Khalil,Hassan K.Nonlinear systems.Macmillan Publishing Company,New York,1992.
[29]Wang G,Ordinary Differential Equation,Higher Education Press,Bei Jing,2005