Formal Verification Of Hybrid Systems And Its Application

The correctness of systems is hard to guarantee owing to the mix and interaction between continuous variables and discrete events of hybrid systems. Especially for the electric power systems and chemical systems, wrong operation will result in fatal loss. The purpose of formal verification is to prove if the hybrid systems operate safely in all conditions.Formal verification is a hotspot as well as difficulty in hybrid systems study. The mature frame and system are not yet built, and the verification tools are still on research state in labs and it is far to extensive application to industry.The main content of this dissertation focuses on formal verification of hybrid systems. The main work in this thesis is as follows:1. On the threshold of domestic research on formal verification of hybrid systems, this thesis summarized various formal verification methods of hybrid systems based on model checking by means of large literature readings, and summed up their essential principle such as computation of reachable set, quotient transition systems, bisimulations and the process of verification. The current main verification tools of hybrid systems were analysed and compared.2. Verification methods of hybrid systems based on flow pipe approximation and partition on threshold switching surface were studied. First, The conception of polyhedral invariant set hybrid automaton and discrete abstract transition systems were introduced. Second, The computation method of finite states approximate quotient transition systems was analysed and it consisted of partition on threshold switching surface, computation of flow pipe, and computation of the states and transition relation in transition systems.3. In the case of linear time invariant continuous dynamic systems and the convex initial region, this thesis presented and proved some deductions about evolvement track of systems. By means of these deductions the improved computation method of transition relation was presented to overcome the difficulty with flow pipe computation, and the improved computation method could save large computation time.4. By means of an instance of inverse pendulum and its control request, this thesispresented its system description and specification description applying to the verification tool CheckMate, verified the inverse pendulum model with CheckMate, and presented the verification result.