Safety verification of state/time-driven hybrid systems using barrier certificates

This paper addresses formal safety verification issue of hybrid systems which resort either state-driven or time-driven strategies. Modeling hybrid systems as linear hybrid automata, we provide a formal method for safety verification by constructing barrier certificates whose existence guarantees the soundness of safety specifications. Barrier certificates for safety of state-driven hybrid systems are presented. Particularly, we propose a formal method for constructing time-dependent barrier certificates and show its sufficiency for safety of time-driven hybrid systems. Through formulating the search of time-dependent barrier certificates as a bilinear sum-of-squares programming problem, a computationally tractable method is proposed to derive a certification on safety in polynomial time. A numerical example illustrates the efficiency of the proposed approach.