Research On Reachable Set Over Approximation Of Hybrid Systems Verification

Hybrid systems are a class of complex dynamic systems composed by discrete events and continuous dynamics which are mixed and interacted with each others. Hybrid systems verification is a research field of hybrid systems. It analyzes whether the reachable sets of system are in target state sets in the case of given initial conditions. The purpose of formal verification is test whether the hybrid system can operate safely in and conditions. Now, the formal verification of hybrid systems became the common and hard research fields in the theory of hybrid systems.Computing reachable sets is an important step in formal verification of hybrid systems. The geometry chosen to represent reachable sets has a deciding effect on the deficiency of the whole procedure. The main content of this dissertation focus on computation of reachable in hybrid systems verification. The main work in this dissertation is as follow:1.This thesis summarized and sorted out various formal methods of hybrid systems by means of large literature readings, and generalized the analysis of reachable sets in formal verification, summarized the main issue of hybrid systems formal verification at the present stage.2. The advantages and disadvantages of reachable sets representation method based on convex hull and oriented rectangular hull were studied deeply by introducing the basic conception of hybrid systems formal verification. A new representation called oriented convex hull method was introduced. This method is a compromise between the impacts of those two methods. Computing complexity of three kinds of representation methods were analyzed by computer tests. The number of vertex and surface geometry which constructs by three kinds of representation method was compared.3. Two conservative judgements of flow pipe, observation comparison and error comparison, were summarized and judgment of error comparison was improved. On this basis, a new conservative judgement of flow pipe, volume comparison was given. The idea of hybrid algorithm which combined by CH and ORH were presented based on the given conservative judgment of plow pipe. 4. The given algorithm of representation method of ORH and hybrid algorithm combined by CH and ORH were implemented in Matlab environment. A section non-linear is taken as an example to be verified,and these two methods are compared from their computation and conservatism. The result showed using the two algorithm presented in this dissertation to verify has a good compromise between computation and conservatism.5. A summary has been done for all discussion in the dissertation. And the research work in the further study is presented.