微信服务号

微信订阅号

2025-4-21- 12
Home > Archive>Volume 27, Issue 3, 2016 >645-654. DOI:10.13328/j.cnki.jos.004986
PDF HTML XML Export Cite reminder
Barrier Certificate Generation for Safety Verification of Continuous Systems for a Bounded Time
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (11271034, 11290141)

  • Article
    • | |
  • Metrics
    • |
  • Reference [22]
    • |
  • Related [20]
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    Barrier certificates have been widely used in verification of continuous systems.The main idea is to find a barrier which separates the reachable set from the unsafe set such that all the trajectories starting from the initial set will never go across the barrier.Thus the system's safety can be guaranteed by constructing a barrier.In recent years, barrier certificates have been successfully used for verification of continuous systems with unbounded time.However sometimes the safety for bounded time needs to be addressed.Since a system is unsafe with unbounded time cannot imply it is also unsafe with a bounded time, the unbounded time barrier certificate method could fail to verify the safety with bounded time.In this paper, a method is presented to generate a bounded time barrier certificate for safety verification of continuous systems with bounded time.Some sufficient conditions for the bounded time barrier certificate are specified.If the continuous system is a polynomial system, relax all the conditions of positive semi-definite polynomial to the sum of squares(SOS) polynomial and then use semi-definite programming(SDP) to solve the conditions for a bounded time barrier certificate;if the continuous system is an elementary system(containing some elementary functions), transform it to a polynomial system approximately, and then solve the corresponding polynomial system for a bounded time barrier certificate.For some practical examples which are unsafe for unbounded time, the paper shows the effectiveness of the proposed method for generating bounded time barriers.

    Reference
    [1] Alur R, Courcoubetis C, Halbwachs N, Henzinger T, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 1995,138(1):3-34.[doi:10.1016/0304-3975(94)00202-T]
    [2] Alur R, Courcoubetis C, Henzinger TA, Ho PH. Hybrid automata:An algorithmic approach to the specification and verification of hybrid systems. In:Proc. of the Hybrid Systems. LNCS 736, Springer-Verlag, 1993. 209-229.[doi:10.1007/3-540-57318-6_30]
    [3] Bu L, Li Y, Wang LZ, Chen X, Li XD. Bach 2:Bounded reachability checker for compositional linear hybrid systems. In:Proc. of the Conf. on Design, Automation and Test in Europe. European Design and Automation Association, 2010. 1512-1517.[doi:10.1109/DATE.2010.5457051]
    [4] Gulwani S, Tiwari A. Constraint-Based approach for analysis of hybrid systems. In:Proc. of the CAV 2008. LNCS 5123, Springer-Verlag, 2008. 19Õ 03.[doi:10.1007/978-3-540-70545-1_18]
    [5] Henzinger TA, Sifakis J. The embedded systems design challenge. In:Proc. of the FM 2006. LNCS 4085, Springer-Verlag, 2006. 1-15.[doi:10.1007/11813040_1]
    [6] Lee E. What's ahead for embedded software? IEEE Computer, 2000,33(9):18-26.[doi:10.1109/2.868693]
    [7] Maler O, Manna Z, Pnueli A. From timed to hybrid systems. In:Proc. of the Real-Time:Theory in Practice, REX Workshop. Springer-Verlag, 1992. 447-484.[doi:10.1007/BFb0032003]
    [8] Zhan NJ, Wang SL, Zhao HJ. Formal modelling, analysis and verification of hybrid systems. In:Proc. of the Unifying Theories of Programming and Formal Engineering Methods. LNCS 8050, Springer-Verlag, 2013. 207-281.[doi:10.1007/978-3-642-39721-9_5]
    [9] Henzinger TA, Ho PH. Algorithmic analysis of nonlinear hybrid systems. In:Proc. of the CAV'95. LNCS 939, Springer-Verlag, 1995. 225-238.[doi:10.1007/3-540-60045-0_53]
    [10] Lafferriere G, Pappas GJ, Yovine S. Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computation, 2001,32(3):231-253.[doi:10.1006/jsco.2001.0472]
    [11] Puri A, Varaiya P. Decidability of hybrid systems with rectangular differential inclusions. In:Proc. of the CAV'94. LNCS 818, Springer-Verlag, 1994. 95-104.[doi:10.1007/3-540-58179-0_46]
    [12] Sanfelice RG, Teel AR. Dynamical properties of hybrid systems simulators. Automatica, 2010,46(2):239-248.[doi:10.1016/j.automatica.2009.09.026]
    [13] Prajna S, Jadbabaie A. Safety verification of hybrid systems using barrier certificates. In:Proc. of the HSCC 2004. LNCS 2993, Springer-Verlag, 2004. 477-492.[doi:10.1007/978-3-540-24743-2_32]
    [14] Kong H, He F, Song XJ, Hung WNN, Gu M. Exponential-Condition based barrier certificate generation for safety verification of hybrid systems. In:Proc. of the CAV 2013. LNCS 8044, Springer-Verlag, 2013. 242-257.[doi:10.1007/978-3-642-39799-8_17]
    [15] Kong H, Song XY, Han D, Gu M, Sun JG. A new barrier certificate for safety verification of hybrid systems. The Computer Journal, 2014,57(7):1033-1045.[doi:10.1093/comjnl/bxt059]
    [16] Dai LY, Gan T, Xia BC, Zhan NN. Barrier certificates revisited. http://arxiv.org/abs/1310.6481
    [17] Dai LY, Xia BC, Zhan NJ. Generating non-linear interpolants by semidefinite programming. In:Proc. of the CAV 2013. LNCS 8044, Springer-Verlag, 2013. 364-380.[doi:10.1007/978-3-642-39799-8_25]
    [18] Löfberg J. Pre-and post-processing sum-of-squares programs in practice. IEEE Trans. on Automatic Control, 2009,54(5):1007-1011. http://users.isy.liu.se/johanl/yalmip/[doi:10.1109/TAC.2009.2017144]
    [19] Parrilo PA. Structured semidefinite programs and semi-algebraic geometry methods in robustness and optimization[Ph.D. Thesis]. California Inst. of Tech., 2000.
    [20] Khalil HK. Nonlinear Systems. 3rd ed., Prentice Hall, 2002.
    [21] Han JJ, Jin Z, Xia BC. Proving inequalities and solving global optimization problems via simplified CAD projection. Journal of Symbolic Computation, 2016,72(2016):206-230.[doi:10.1016/j.jsc.2015.02.007]
    [22] Liu J, Zhan NJ, Zhao HJ, Zou L. Abstraction of elementary hybrid systems by variable transformation. In:Proc. of the FM 2015. LNCS 9109. 2015. 360-377.[doi:10.1007/978-3-319-19249-9_23]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

甘庭,夏壁灿.运用栅栏函数验证连续系统的有界时间安全性.软件学报,2016,27(3):645-654

Copy
Share
Article Metrics
  • Abstract:5065
  • PDF: 6374
  • HTML: 2542
  • Cited by: 0
History
  • Received:July 16,2015
  • Revised:October 20,2015
  • Online: January 06,2016
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2036622Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063