Font Size: a A A

Safety Verification Of Continuous Systems With Neural Network Controllers Via Barrier Certificates

Posted on:2022-02-10Degree:MasterType:Thesis
Country:ChinaCandidate:M ShaFull Text:PDF
GTID:2518306725481334Subject:Computer technology
Abstract/Summary:PDF Full Text Request
Deep neural network has proved its potential to replace human intelligence in decision making in many complex application scenarios.A large number of deep neural network controllers are embedded in the cyber-physical systems for intelligent control.However,the black box nature,large number of neurons and nonlinear characteristics of the neural networks make it difficult to understand and analyze its behavior.In particular,how to ensure that the safety critical systems controlled by deep neural networks meet the necessary safety requirements becomes an urgent and extremely challenging problem.Modeling these safety critical cyber-physical systems with hybrid systems and verifying whether the behavior satisfies the security nature based on formal verification techniques is the most effective way to guarantee the security property.Existing works try to verify the safety of those systems by calculating the reachable set or constructing barrier certificates based on data-driven method.However,reachable set based methods can only verify the security within a limited time horizon while the data-driven barrier certificate construction methods are influenced by the sample data and the success rate is not high when facing high dimensional systems.To solve the above problems,we propose two barrier certificate construction methods to verify the security of the hybrid systems controlled by deep neural networks.Different from the data-driven method,these two methods can directly generate the barrier certificates of the system to be verified by constructing the approximation system,which has a higher success rate.Specifically,the main research works of this paper are as follows:1 A novel barrier certificate generation method based on polynomial abstraction system is proposed for the first time.The core idea is to abstract the DNN controller by polynomials,and evaluate the error bound between the two based on the real trajectories of the system,so as to transform the originally complex DNN controller into a polynomial controller with error,and construct an abstract semi-algebraic hybrid system to generate the candidate barrier certificate of the original system.Then an SMT solver is used to select the real barrier certificate from these candidate barrier certificates.In order to overcome the side effect caused by the abstraction error,an iterative framework was designed to improve the success rate of the generation by moderately expanding the upper bound of the error estimation.Compared with the existing candidate barrier certificate generation methods based on simulation,the proposed algorithm is more stable and efficient.2 The method of generating barrier certificate based on approximation system is proposed for the first time.The data-driven barrier certificate generation method is limited by the verification ability of the back-end SMT solvers,and it cannot be verified in limited time for some high dimensional systems and high complexity controllers.Therefore,this paper proposes a direct barrier certificate generation method.In this method,Bernstein polynomial approximation is introduced to construct an approximate semi-algebraic system,and Bernstein's generalization theorem is used to obtain a strict upper bound on the error between the approximating polynomial and the original neural network controller,which ensures that the generated approximation semi-algebraic system is a strict closure of the original one.It also means that the barrier certificate of the approximate semi-algebraic system must also be a barrier certificate of the original system.In order to alleviate the problem of large approximation error of Bernstein polynomials,an iterative verification framework based on partition is further proposed,which can effectively transform the original problem into multiple subproblems to reduce the computational complexity.This algorithm breaks through the calculation bottleneck of data-driven barrier certificate generation algorithms and greatly expands the scale of verifiable system.3 Develop prototype tools and complete comparative experiments.Based on the above work,this paper designs and implements two prototype tools to evaluate the effectiveness of the algorithms on a set of benchmarks,and com-pares it with state-of-the-art work.Experimental results show that the two methods proposed in this paper significantly improve the success rate of barrier certificate generation and the scale of the verifiable problem compared with the existing work.
Keywords/Search Tags:Hybrid system, Neural network controller, Barrier certificate, Safety verification
PDF Full Text Request
Related items