Inductive Invariant Based Safety Verification Of Hybrid Systems

Researches on embedded systems are attracting more and more attention as em-bedded systems are widely used in safety-critical areas. Hybrid systems are ideal formalmodels for embedded systems since they can specify both discrete control logics and con-tinuous behaviors of plants in embedded systems. Safety verification is among the mostchallenging problems in verifying hybrid systems. However, the verification methods fordiscrete systems are not applicable to hybrid systems due to their continuous behaviors,which means that we have to develop new methods for the safety verification of hybridsystems.In this thesis, we aims to solve the problems in the inductive invariant based safetyverification of hybrid systems and our work consists of three parts: the evaluation rule ofinductive conditions, the definition of inductive conditions and the constructing methodsof inductive invariants. The main contributions of our work are as follows:primarily establish a set of evaluation rules for hybrid system inductive conditionswhich helps to gain a deep understanding of inductive conditions and to guide thedesigning of better inductive conditions and better inductive invariant generatingmethods and thereby lays a solid foundation for the future research on inductiveinvariants.propose an inductive invariant (called barrier certificate) generation method basedon the exponential condition and semi-definite programming method. Theinductive invariant based on exponential condition can form a precise over-approximation for the reachable set of the system and hence can verify the safetyproperty where the unsafe region is very close to the reachable region. In addition,exponential condition is convex and hence can be solved efciently by semi-definiteprogramming.propose an inductive invariant generation method based on a complete induc-tive condition and quantifier elimination. Compared with the above method, thismethod is complete, hence, it possesses the greatest verification power. Comparedwith the existing complete inductive condition, the condition in this thesis can beeasily adapted to obtain a set of sufcient inductive conditions with diferent level ofconservativeness and computational complexity, which provides us with a means to trade of between verification power and computational complexity. An algorithmbased on quantifier elimination and SMT is designed for generating inductive in-variants.implement a tool, called HIIDiscoverer, for automatically and efciently generat-ing hybrid system inductive invariants.