Safety Verification Of Hybrid Systems Based On Barrier Certificate Generation

Hybrid system is a class of very complicated dynamical system,whose behavior is tangled with continuous evolutions and discrete transitions.Its continuous behaviour can be used to model the independent hardwares and its discrete behaviour can describe the switch of different modes.Therefore,it suits well for the task of modelling the embed-ding systems and also the cyber-physical systems(CPS)developed from the embedding systems.With the rapid development of information technology and manufacturing en-gineering,the embedding systems and CPS are widely used in safety-critical areas like aeronautics and astronautics,transportation,medical and health science,etc.Through mathematical methods and computer techniques,the study of the safety verification prob-lem of hybrid systems becomes a hot frontier research topic,which is a very important subject both in theory and in practice.One of the popular methods for safety verification of hybrid systems is the barrier certificate generation method which has the advantage of avoiding the computation of the reachable sets.There are two key aspects of this kind of methods:on one side,the current barrier certification constructing relies on some conservative conditions;on the other side,computing the constraints for barrier certificates has very high complexity.Therefore,the focus of this thesis is to study the barrier certificates method from three aspects:how to generate barrier certificate with more relaxed constraints,how to simplify the computation of the model of the barrier certificate,how to abstract the model to lower the complexity of the symbolic algorithms for generating the barrier certificate.The main contributions of this thesis are summarized as follows:·We provide a novel method for generating the barrier certificates.Our method us-es the Darboux polynomial to construct a new class of barrier certificate,which is called Darboux barrier certificate generation method.Using this new generation method,we can generate barrier certificate functions which existing methods fail to generate,and it is illustrated by experiments.Moreover,using some special form of the Darboux barrier certificate model,we present a new LS-QP cross projec-tion method,which can compute the Darboux barrier certificates very efficiently.Experiments show that our algorithm has high efficiency..We propose a new method for computing barrier certificates based on a BMI model.The BMI model is converted from classical differential barrier certificate model through SOS relaxation method.We first study the general BMI problem and give the explicit formula of each step of the alternating direction Lagrangian method for solving the BMI problem.Then we apply this result for computing the barrier certificates and design an algorithm for safety verificaton.At last,we compare our algorithm with the one used in PENNON,which shows our algorithm has lower complexity.·We present a new abstraction method.We start from the complicated nonlinear hybrid system to construct linear abstraction model.Using the linear model from abstraction,we transform the nonlinear hybrid system into a linear system with parameters for further verification,which avoids the high complexity for generat-ing barrier certificates of the complicated original system.First,we transform the nonlinear hybrid system into a linear system with parameters.Then the method of quantifiers elimination is used to generate linear barrier certificates.The safety property of the parametric linear model guarantees the safety of the original system.Our experiments illustrate that the linear abstraction method succeed to generate barrier certificates which can not be achieved by using the method of quantifiers elimination directly.