Increasing penetration of renewable energy introduces significant uncertainty into power systems. Traditional simulation-based verification methods may not be applicable due to the unknown-but-bounded feature of the uncertainty sets. Emerging set-theoretic methods have been intensively investigated to tackle this challenge. The paper comprehensively reviews these methods categorized by underlying mathematical principles, that is, set operation-based methods and passivity-based methods. Set operation-based methods are more computationally efficient, while passivity-based methods provide semi-analytical expression of reachable sets, which can be readily employed for control. Other features between different methods are also discussed and illustrated by numerical examples. A benchmark example is presented and solved by different methods to verify consistency.
A small-gain theorem in the formulation of barrier function is developed in this work for safety verification of interconnected systems. This result is helpful to verify input-to-state safety (ISSf) of the overall system from the safety information encoded in the subsystem's ISSf-barrier function. Also, it can be used to obtain a safety set in a higher dimensional space from the safety sets in two lower dimensional spaces.
Modern safety-critical energy infrastructures are increasingly operated in a hierarchical and modular control framework which allows for limited data exchange between the modules. In this context, it is important for each module to synthesize and communicate constraints on the values of exchanged information in order to assure system-wide safety. To ensure transient safety in inverter-based microgrids, we develop a set invariance-based distributed safety verification algorithm for each inverter module. Applying Nagumo's invariance condition, we construct a robust polynomial optimization proble…
Computer Science and Artificial Intelligence Laboratory (CSAIL)（计算机科学与人工智能实验室（CSAIL））；Massachusetts Institute of Technology (MIT)（麻省理工学院（MIT））
In this paper, we address the real-time risk-bounded safety verification problem of continuous-time state trajectories of autonomous systems in the presence of uncertain time-varying nonlinear safety constraints. Risk is defined as the probability of not satisfying the uncertain safety constraints. Existing approaches to address the safety verification problems under uncertainties either are limited to particular classes of uncertainties and safety constraints, e.g., Gaussian uncertainties and linear constraints, or rely on sampling based methods. In this paper, we provide a fast convex algori…
This paper develops a small-gain technique for the safety analysis and verification of interconnected systems with high-relative-degree safety constraints. In this technique, input-to-state safety (ISSf) is used to characterize how the safety of a subsystem is influenced by the external input, and ISSf-barrier functions (ISSf-BFs) with high relative degree are employed to capture the safety of subsystems. With a coordination transform, the relationship between ISSf-BFs and the existing high-relative-degree (or high-order) barrier functions is established in order to simplify the ISSf analysis.…
Artificial neural networks have recently been utilized in many feedback control systems and introduced new challenges regarding the safety of such systems. This paper considers the safe verification problem for a dynamical system with a given feedforward neural network as the feedback controller by using a constrained zonotope-based approach. A novel set-based method is proposed to compute both exact and over-approximated reachable sets for neural feedback systems with linear models, and linear program-based sufficient conditions are presented to verify whether the trajectories of such a syste…
The deployment of autonomous systems that operate in unstructured environments necessitates algorithms to verify their safety. This can be challenging due to, e.g., black-box components in the control software, or undermodelled dynamics that prevent model-based verification. We present a novel verification framework for an unknown dynamical system from a given set of noisy observations of the dynamics. Using Gaussian processes trained on this data set, the framework abstracts the system as an uncertain Markov process with discrete states defined over the safe set. The transition bounds of the …
Formal Safety Verification for Nonlinear Systems with Generative Barrier Certificate
Shanghai Key Lab of Trustworthy Computing, East China Normal University（华东师范大学）；College of Computer Science and Technology, National University of Defense Technology（国防科技大学计算机学院）
In this paper we consider the safety verification and safe controller synthesis problems for nonlinear control systems. The Control Barrier Certificates (CBC) approach is proposed as an extension to the Barrier certificates approach. Our approach can be used to characterize the control invariance of a given set in terms of safety of a general nonlinear control system subject to input constraints. From the point of view of controller design, the proposed method provides an approach to synthesize a safe control law that guarantees that the trajectories of the system starting from a given initial…
In this paper, we consider the problem of verifying safety constraint satisfaction for single-input single-output systems with uncertain transfer function coefficients. We propose a new type of barrier function based on a vector norm. This type of barrier function has a measurable upper bound without full state availability. An identifier-based estimator allows an exact bound for the uncertainty-based component of the barrier function estimate. Assuming that the system is safe initially allows an exponentially decreasing bound on the error due to the estimator transient. Barrier function and e…
With the growing interest in deploying robots in unstructured and uncertain environments, there has been increasing interest in factoring risk into safety-critical control development. Similarly, the authors believe risk should also be accounted in the verification of these controllers. In pursuit of sample-efficient methods for uncertain black-box verification then, we first detail a method to estimate the Value-at-Risk of arbitrary scalar random variables without requiring \textit{apriori} knowledge of its distribution. Then, we reformulate the uncertain verification problem as a Value-at-Ri…
Deep learning methods can be used to produce control policies, but certifying their safety is challenging. The resulting networks are nonlinear and often very large. In response to this challenge, we present OVERT: a sound algorithm for safety verification of nonlinear discrete-time closed loop dynamical systems with neural network control policies. The novelty of OVERT lies in combining ideas from the classical formal methods literature with ideas from the newer neural network verification literature. The central concept of OVERT is to abstract nonlinear functions with a set of optimally tigh…
School of Aeronautics and Astronautics（航空航天学院）；Purdue University（普渡大学）
Model-based reinforcement learning (RL) has emerged as a promising tool for developing controllers for real world systems (e.g., robotics, autonomous driving, etc.). However, real systems often have constraints imposed on their state space which must be satisfied to ensure the safety of the system and its environment. Developing a verification tool for RL algorithms is challenging because the non-linear structure of neural networks impedes analytical verification of such models or controllers. To this end, we present a novel safety verification framework for model-based RL controllers using re…
We present a safety verification framework for design-time and run-time assurance of learning-based components in aviation systems. Our proposed framework integrates two novel methodologies. From the design-time assurance perspective, we propose offline mixed-fidelity verification tools that incorporate knowledge from different levels of granularity in simulated environments. From the run-time assurance perspective, we propose reachability- and statistics-based online monitoring and safety guards for a learning-based decision-making model to complement the offline verification methods. This fr…
The goal of this paper is to analyze Long Short Term Memory (LSTM) neural networks from a dynamical system perspective. The classical recursive equations describing the evolution of LSTM can be recast in state space form, resulting in a time-invariant nonlinear dynamical system. A sufficient condition guaranteeing the Input-to-State (ISS) stability property of this class of systems is provided. The ISS property entails the boundedness of the output reachable set of the LSTM. In light of this result, a novel approach for the safety verification of the network, based on the Scenario Approach, is…
This paper presents the design of a supervisory algorithm that monitors safety at road intersections and overrides drivers with a safe input when necessary. The design of the supervisor consists of two parts: safety verification and control design. Safety verification is the problem to determine if vehicles will be able to cross the intersection without colliding with current drivers' inputs. We translate this safety verification problem into a jobshop scheduling problem, which minimizes the maximum lateness and evaluates if the optimal cost is zero. The zero optimal cost corresponds to the ca…
University of Oxford（牛津大学）；Paderborn University（帕德博恩大学）
Hamilton-Jacobi reachability methods for safety-critical control have been well studied, but the safety guarantees derived rely on the accuracy of the numerical computation. Thus, it is crucial to understand and account for any inaccuracies that occur due to uncertainty in the underlying dynamics and environment as well as the induced numerical errors. To this end, we propose a framework for modeling the error of the value function inherent in Hamilton-Jacobi reachability using a Gaussian process. The derived safety controller can be used in conjuncture with arbitrary controllers to provide a …
In this letter, we detail our randomized approach to safety-critical system verification. Our method requires limited system data to make a strong verification statement. Specifically, our method first randomly samples initial conditions and parameters for a controlled, continuous-time system and records the ensuing state trajectory at discrete intervals. Then, we evaluate these states under a candidate barrier function $h$ to determine the constraints for a randomized linear program. The solution to this program then provides either a probabilistic verification statement or a counterexample. …
In this paper, we propose a data-driven approach to formally verify the safety of (potentially) unknown discrete-time continuous-space stochastic systems. The proposed framework is based on a notion of barrier certificates together with data collected from trajectories of unknown systems. We first reformulate the barrier-based safety verification as a robust convex problem (RCP). Solving the acquired RCP is hard in general because not only the state of the system lives in a continuous set, but also and more problematic, the unknown model appears in one of the constraints of RCP. Instead, we le…
We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map solutions and to other solutions. We show that this property can be used to transform cached reachsets to compute new reachsets, for hybrid and multi-agent models. We develop a notion of virtual system which define symmetry transformations for a broad class of agent models that visit waypoint sequences. Using this notion of virtual system, we present a prototype tool CacheReach that builds a cache of reachtubes for this system, in a wa…
The well-known quote from George Box states that: "All models are wrong, but some are useful." To develop more useful models, we quantify the inaccuracy with which a given model represents a system of interest, so that we may leverage this quantity to facilitate controller synthesis and verification. Specifically, we develop a procedure that identifies a sim2real gap that holds with a minimum probability. Augmenting the nominal model with our identified sim2real gap produces an uncertain model which we prove is an accurate representor of system behavior. We leverage this uncertain model to syn…
Safety Verification for Evasive Collision Avoidance in Autonomous Vehicles with Enhanced Resolutions
New York University（纽约大学）；North Carolina A&T State University（北卡罗来纳农工州立大学）；University of Notre Dame（圣母大学）；Qualcomm（高通公司）；Torc Robotics（托尔克机器人公司）；Glasgow Caledonian University（格拉斯哥卡里多尼亚大学）；American Axle & Manufacturing（美国车桥制造公司）；Gatik AI（加蒂克人工智能公司）
Automated Driving is revolutionizing many of the traditional ways of operation in the automotive industry. The impact on safety engineering of automotive functions is arguably one of the most important changes. There has been a need to re-think the impact of the partial or complete absence of the human driver (in terms of a supervisory entity) in not only newly developed functions but also in the qualification of the use of legacy functions in new contexts. The scope of the variety of scenarios that a vehicle may encounter even within a constrained Operational Design Domain, and the highly dyn…
A Verification Methodology for Safety Assurance of Robotic Autonomous Systems
Faculty of Science and Technology, Norwegian University Of Life Sciences (NMBU)（科学与技术学院，挪威生命科学大学）；Department of Mechatronics, University of Agder (UiA)（机械电子系，阿格德大学）；Department of Computer Science, University Of York, UK（计算机科学系，约克大学（英国））
A fail-operational system for highly automated driving must complete the driving task even in the presence of a failure. This requires redundant architectures and a mechanism to reconfigure the system in case of a failure. Therefore, an arbitration logic is used. For functional safety, the switch-over to a fall-back level must be conducted in the presence of any electric and electronic failure. To provide evidence for a safety argumentation in compliance with ISO 26262, verification of the arbitration logic is necessary. The verification process provides confirmation of the correct failure rea…
Quantifying the robustness of neural networks or verifying their safety properties against input uncertainties or adversarial attacks have become an important research area in learning-enabled systems. Most results concentrate around the worst-case scenario where the input of the neural network is perturbed within a norm-bounded uncertainty set. In this paper, we consider a probabilistic setting in which the uncertainty is random with known first two moments. In this context, we discuss two relevant problems: (i) probabilistic safety verification, in which the goal is to find an upper bound on…
As control systems become increasingly more complex, there exists a pressing need to find systematic ways of verifying them. To address this concern, there has been significant work in developing test generation schemes for black-box control architectures. These schemes test a black-box control architecture's ability to satisfy its control objectives, when these objectives are expressed as operational specifications through temporal logic formulae. Our work extends these prior, model based results by lower bounding the probability by which the black-box system will satisfy its operational spec…
Control systems often must satisfy strict safety requirements over an extended operating lifetime. Control Barrier Functions (CBFs) are a promising recent approach to constructing simple and safe control policies. This paper proposes a framework for verifying that a CBF guarantees safety for all time and synthesizing CBFs with verifiable safety in polynomial control systems. Our approach is to show that safety of CBFs is equivalent to the non-existence of solutions to a family of polynomial equations, and then prove that this nonexistence is equivalent to a pair of sum-of-squares constraints v…
Norwegian University of Science and Technology（挪威科技大学）；Southwest Jiaotong University（西南交通大学）
Context: Neural Network (NN) algorithms have been successfully adopted in a number of Safety-Critical Cyber-Physical Systems (SCCPSs). Testing and Verification (T&V) of NN-based control software in safety-critical domains are gaining interest and attention from both software engineering and safety engineering researchers and practitioners. Objective: With the increase in studies on the T&V of NN-based control software in safety-critical domains, it is important to systematically review the state-of-the-art T&V methodologies, to classify approaches and tools that are invented, and to identify c…
Northwestern University（西北大学）；UC Berkeley（加州大学伯克利分校）；University of Liverpool（利物浦大学）；Yale University（耶鲁大学）
In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties (e.g., safety, stability) under the learned controller. However, as existing methods typically apply formal verification \emph{after} the controller has been learned, it is sometimes difficult to obtain any certificate, even after many iterations between learning and verification. To address this challenge, we propose a framework that jointly conducts reinforcement learning and formal verification by formulating and solving a novel bilevel optimization problem, which…
