The Abstraction And Formalized Verification Of Heating Hybrid System

In the heating system, water, as the medium and carrier of heat energy, its pressure level influences the heating quality and the safe operation of system directly. Heating system comprised of continuous system (such as the change of water pressure), and discrete system (such as the turning on or turn off of water pump), so heating system belong to typical hybrid dynamic system. In the face of the requisition for control technology and systematic complexity Increased day by day, the exactness and dependability of hybrid system are particularly important.The formal verification of hybrid system includes the automatic verification of model examination by algorithm, and artificial or machinery verification utilizing deduction certification. This thesis combines the two methods. First, change the heating dynamic system into a discrete abstraction system by means of qualitative reasoning method. Second, set up a discrete state model diagram with figure modeling tool Stateflow in Matlab. Last, adopt the symbol model verification tool SMV to prove the discrete state model automatically. Due to state space explosion problem in heating hybrid system formal verification, this thesis expands the qualitative reasoning method, on the basis of nth derivation in the real space, change the heating dynamic system into a discrete abstraction system. While preserving some of its relevant behavior, the simplified system is more accessible to analysis tools and is still sufficient to establish certain safety properties.Moreover, the thesis adopts the symbol model verification tool SMV to prove the discrete state model automatically. SMV, based on OBDDs (ordered binary decision diagrams) searching algorithm to determine whether the system satisfy the properties described by CTL (Computation Tree Logic). The symbol denotation method is very natural to the modeling of the digital circuit, and can verify the system with great state space. It is used to automatically verify the discrete system after being abstracted in this thesis.The division of the state space of hybrid system is the focal point in system verification, so in the end of the thesis, we discuss other kinds of division methods and compare them one by one. In addition, the method taken in the thesis is equally suitable with other hybrid system.