Analysis Of Hybrid System Formal Verification Modeling Tools

Hybrid systems formal verification is a mathematically-based technology for specifying the hybrid system's safety porperty. In recent ten years, model verification technology is the main method of formal verification. Model verification is to verify if a system satisfies the designing requirements by traversal search algorithms using computer to automatically check all states space through and convergently or over-approximately computing possible trajectories.In this thesis, the conception and characters of modeling verification has been firstly introduced, and then the useful modeling methods such as hybrid automaton, hybrid Petri net, hierarchical structure and duration calculus. The front computing method, backward computing method and over-approximated method for reachable sets have been systematically anglicized. Finally introduce the native and abroad researching status and useful modeling tools.Due to the character of hybrid system that not only include continuous subsystem and discrete subsystem, investigate the hybrid automaton, polyhedron hybrid automaton and hybrid input and output automaton. For the problem of over-approximated flow pipe, the new over-approximated polyhedron zonotopes which represent the reachable sets based on the center and generators. Analyze the conservative and close property, intersection and convergence. Through comparing adaptive system, computing method and computing complexity, tells the advantages and disadvantages from convex hull and zonotopes.Build mathematic model, abstract the verification questions, provide the ACTL specification for atmospheric pressure oven heating system (linear system) and automobile adaptive cruise system (nonlinear system). Use PHAVer and CheckMate to construct the hybrid system respectively, apply zonotopes polyhedral and convex hull to over-approximated flow pipe for verifing models, analyzing the state reachability and safety property for the above mentioned hybrid system. Through analyzing the conservative property, time consumption and output file size, comparing the advantages and disadvantages of CheckMate and PHAVer.