The Methods Of Linear Hybrid System Formal Verification And Its Application

Hybrid systems are a class of complex dynamic systems composed by linear subsystem and discrete subsystem which are interacted with each other. Linear and discrete subsystem are interacted, the system's function track was discrete state transition holistically, the stepwise evolvement of linear state is presented partly ,the much complex dynamic action was appeared ,it is very difficult that analysis of the hybrid systems function's security and state's reachability.All tasks were worked for linear hybrid system formal verification. Linear system has the characteristic that its reachable set is convex hull if its initial region is convex hull. The subsystem is linear system in the hybrid system`s invariable set.The linear hybrid system verification process can be simplified.This thesis used crude oil heat process as example, it was modelled, the system was verified by the formal verification technique based on flow pipe and simplified flow pipe, the system's security and reachability was analyzed,this provided a reference for linear hybrid system verification.The main work in this thesis is as follows:1. The verification method based on flow pipe is analyzed, includes: the necessary of partition was analyzed, over approximate flow pipe, the relationship of over approximate flow pipe and quotient transition systems' establishment was analyzed.2. The verification tools were compared. CheckMate was a verification tool based on flow pipe, its function models was introduced in detail.3. The crude oil heater process run principle is analyzed,based on that the dynamical model is built,the verification problem is abstracted; hybrid automata model is established, the system`s state reachablity and function security is analyzed used the verification method based on flow pipe, verification result is worked out. The influence on the verification result used the different step in the verification process.4. The crude oil heat process was verified by the verification method based on simplified flow pipe, The verification result was presented and analyzed. There is a compare between the verification results, they were presented by verification method based on flow pipe and simplified flow pipe. Their conservatism and computation costs were analyzed.