The Research On Formal Verification Of Hybrid Systems

Hybrid system theory lies at the intersection of the fields of engineering control theory and computer science verification. It is defined as the modeling, analysis, control and verification of systems that involve the interaction of both discrete state system, represented by finite automata, and continuous state dynamics, represented by differential equations. To understand the behavior of hybrid systems and to verify whether the hybrid systems operate safely in some conditions, theoretical advances and analyses tools are needed. Formal verification is a hotpot as well as difficulty in hybrid systems study. The mature frame and system are not yet built, and verification tools are still on research state in labs, witch are difficult to extensive the application to industrial objects.In this thesis, the main content of this dissertation focuses on formal verification of hybrid systems. The research pivot is to solve the difficulties of discrete model approximation of continuous dynamics, where reach set computation is a main task. Aim at computing difficulty of flow pipe approximation in non-linear systems, this thesis presents a variable time interval method of flow pipe approximation; And according to property of flow pipe approximation, the approaching method of flow pipe and of polyhedron are given witch can be defined as computing flow pipe approximation near the switch surface.A new method of computing reachable set on switch face is presented based on analysising the principle about the method of flow pipe approximation. The method works out the least convex polyhedron that enwraps the real reachable set on switch face. And the real reachable set is obtained by below approach. Fast of all, working out the numerical value on switch face for a dot in initial area, then inbed the numerical value in optimizing program to obtain the real reachable set.A partition method based on counterexample is discussed, witch partition the state in respect of verification criterion, so the problem of state exploding caused by partitioning state space once more is avoided in a way. When partitioning counterexample state, there is no effective method partitioning the counterexample state into litter state corresponding to the latter state of counterexample state, due to the above reason, a partition method of half cutting is presented. This method can find out the relation between the latter state of counterexample state and the litter state after partitioned the counterexample.In experiment part of thesis, we verify the model of invert pendulum with verification tool of CheckMate. And we present an experiment result thought counterexample partition. For the more, we gain some experiment results about computing reachable set thought some method provided in this thesis and analysis the result in contrast to original method, thought witch we expatiate the feasibility about those methods.Finally, sum up the content of this thesis and analysis deficiency in research. And research work in the further study is presented.