Hybrid System Verification Using Reachable Set Over Approximations

Hybrid systems (HSs) are a class of complex dynamic systems composed by discrete events and continuous dynamics which are mixed and interacted with each other. With the increasing application of microcomputers, microprocessors and large-scale communication network, as well as the emergence of man-made systems in industry, the theories and applications of HS became the common research fields in computer science and control communities during the last two decades.Firstly, background and the research actuality of HS are reviewed, and the conception, characteristic and significance on HS research are introduced. The similarities and differences between simulation and formal verification have been presented, at the mean time, the current main verification tools of hybrid systems are analyzed and compared.HS modeling methods based on hybrid automata are studied. For the infinite state transition problem in HS verification, model checking using state space exploration method is analyzed. Computation tree logic and action based temporal logical, which are both important methods in system verification, is presented.The advantages and disadvantages of reachable sets representation method based on convex polyhedron, rectangular hull and oriented rectangular hull are compared in conservatism, computation costs, performing operations like union and intersection, at the same time, the faces and vertices increase with the dimension. And the principle of representation and computation method of reachable sets is presented.Verification methods of hybrid systems based on flow pipe approximation and partition on threshold switching surface are studied. The method of finite states approximate quotient transition systems is analyzed, which includes the discretization of the switching surfaces, flow pipe approximations, the computation of the transition relation and the quotient transition system refinement. According to the character of the linear time-invariant system and the properties of convex polyhedron, the evolving rules of the reachable set of the system are presented and proved. By means of these rules, the computation of the transition relation in the hybrid system verification is simplified and the algorithm by combining vertices simulation and flow pipe approximation is presented, as well as the calculate process and procedural block are provided.Taking two examples, the differences between flow pipe approximation and the algorithm by combining vertices simulation and flow pipe approximation were compared. Then, according to the method suggested by the author, the verification procedure is compiled, and the verification process is illustrated, and furthermore, these two methods are compared from their computation costs and conservatism.Finally, a summary has been done for all discussion in the thesis. And the research work in the further study is presented.