Research And Applications Of Flow Pipe Approximation Methods In Formal Verification Technology

Hybrid systems 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, the theories and applications of Hybrid systems became the common research fields in computer science and control communities during the last two decades.Firstly, the concepts and typical examples of hybrid systems are introduced.The methods of modeling, analysising, verifying hybrid systems are systematically described.The current research situation, verification tools and basic concept of formal verification are detailedly introduced.Hybrid system modeling methods based on hybrid automata are studied. For the infinite state transition problem in hybrid system 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.The flow pipe approximation method is an important content of formal verification technology. According to difference of continous dynamics, hybrid sytem is classified as clock linear and nonlinear systems.For each type hybrid sytem,they have different flow pipe approximation method.This paper described detailedly their flow pipe approximation method for the three type hybrid systems,and concertration control system(clock),chemical evaporation system(nonlinear) and atmospheric pressure oven heating system(linear) are used as research object.Based on the analysis of continuous and discrete part of the above system,the hybrid automata model is created,the specification to verify is presented.By using their own flow pipe approximation method, the verification result is given finally.