Abstract—This paper investigates safety verification for
hybrid automata with transient safe modes. Safety properties
might be violated by solely transient safe modes in some finite
time, with respect to permanently safe modes. A new kind of
barrier certificate with time constraints is proposed to derive a
criterion for safety of such kind of hybrid automata. The
improved barrier certificates are more suitable for hybrid
automata whose safety heavily relies on well-defined real-time
scheduling. With the help of numerical solvers such as
SOSTOOLS or SOSOPT for MATLAB, the proposed barrier
certificates could be computed by solving some sum-of-squares
program as well as bilinear sum-of-squares program problems.
The validity of the proposed verification method is supported by
a numerical example.
Index Terms—Formal methods, hybrid system, safety
verification.
Guobin Wang is with the School of Computer Science and Software
Engineering, East China Normal University, Shanghai 200062, China
(e-mail: guobin_hyb_ver@126.com).
Jing Liu is with Shanghai Key Laboratory of Trustworthy Computing,
National Trustworthy Embedded Software Engineering Technology
Research Center, East China Normal University, Shanghai 200062, China
(e-mail: jliu@sei.ecnu.edu.cn).
[PDF]
Cite: Guobin Wang and Jing Liu, "Safety Verification of Hybrid Automata with Transient
Safe Modes," International Journal of Modeling and Optimization vol. 6, no. 4, pp. 238-245, 2016.
