Formal Verification Of Hybrid Systems

A hybrid system is a dynamical system with both discrete and continuous state changes,which is broadly applied to complex engineering,including air-traffic control, automotive control,robotics and manned space flight.In particular,the high-confidence and safety-critical nature of the application areas has fostered a large and growing body of work on formal methods for hybrid systems.There are mainly two types of formal verification techniques:theorem proving and model checking.The latter is typically based on a technique known as reachability analysis.Due to the infinite state-spaces of hybrid systems,researchers mainly care for the reachability analysis of hybrid systems,because only small subclasses of hybrid systems have decidable teachability.For the reachability analysis of hybrid systems,researchers use convex polyhedra or structures similar to polyhedra to represent the set of states,and use a procedure of quantifier elimination,which has a double exponential complexity, to compute the reachability states.The investigation of the model checking problems of hybrid systems mainly focuses on the field of real-time systems,which can be seen as a simple sub-case of hybrid systems.This thesis firstly investigates the satisfiability of a subset of the first order projection temporal logic which is defined over finite integers.Besides,we define a dense timed interval temporal logic(DTITL)to describe properties of real-time and hybrid systems,and prove that the satisfiability of DTITL is decidable by translating it to the same issue for the first order projection temporal logic over finite integers.This thesis also formalizes a constraint system called hybrid zone to deal with symbolic teachability analysis of rectangular hybrid systems.A hybrid zone is a conjunction of inequalities that compare either a variable or a linear expression of two variables to a rational number.Hybrid zones are proved to be closed over the state reachability operations for rectangular hybrid systems.To represent hybrid zones,a matrix data structure called difference constraint matrix(DCM)is defined.After the DCM has been converted to canonical form,the reachability operations for rectangular hybrid systems can be implemented straightforwardly.Thus,the main computation is the operation for obtaining canonical form.Finding the canonical form is an issue of linear programming which can be automated by an algorithm with polynomial time complexity. To handle unions of hybrid zones,a rectangular hybrid diagram is formalized.In addition,we introduce a method for translating nonlinear hybrid systems into rectangular hybrid automata.Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated rectangular hybrid automata.To deal with the model checking problem for multirate hybrid systems,that is,to check whether a multirate hybrid automaton M satisfies a DTITL formulaφ,an equivalent relation of valuations is defined in this thesis to construct a region automaton A from M.Besides,a propositional projection temporal logic formulaψis constructed fromφ. Then,it is proved that M satisfiesφiff A satisfiesψ.The latter is a model checking problem for propositional projection temporal logic.There already exist algorithms for solving this problem.Finally,this thesis simplifies the hybrid projection temporal logic(HPTL),and gives a collection of logic laws of HPTL.Using these logic laws,we can prove properties of hybrid systems with the theorem proving technique.To show this,an example is given in detail.