Search

This paper presents an overview survey of verification techniques for autonomous systems, with a focus on safety-critical autonomous cyber-physical systems (CPS) and subcomponents thereof. Autonomy in CPS is enabled by recent advances in artificial intelligence (AI) and machine learning (ML) through approaches such as deep neural networks (DNNs), embedded in so-called learning enabled components (LECs) that accomplish tasks from classification to control. Recently, the formal methods and formal verification community has developed methods to characterize behaviors in these LECs with eventual goals of formally verifying specifications for LECs, and this article presents a survey of many of these recent approaches.

In this note, a novel conception called virtual clock, which is defined by an artificial timer over a finite cycle, is introduced for stability analysis of discrete-time switched linear systems under minimum dwell-time constraint. Two necessary and sufficient conditions associated with a virtual clock with a sufficient length are proposed to ensure the global uniform asymptotic stability of discrete-time switched linear systems. For the two nonconservative stability criteria, the lifted version maintains the convexity in system matrices. Based on the lifted convex conditions, the extensions to $\ell _2$ -gain computation and $\mathcal {H}_\infty$ control problems are presented in the sequel. In particular, a novel virtual-clock-dependent controller is designed, which outperforms the traditional mode-dependent and common gain controllers. Several numerical examples are provided to illustrate our theoretic results.

In this brief, the output reachable estimation and safety verification problems for multilayer perceptron (MLP) neural networks are addressed. First, a conception called maximum sensitivity is introduced, and for a class of MLPs whose activation functions are monotonic functions, the maximum sensitivity can be computed via solving convex optimization problems. Then, using a simulation-based method, the output reachable set estimation problem for neural networks is formulated into a chain of optimization problems. Finally, an automated safety verification is developed based on the output reachable set estimation result. An application to the safety verification for a robotic arm model with two joints is presented to show the effectiveness of the proposed approaches.

In this note, the global exponential stability of discrete-time switched systems under arbitrary switching is investigated. First, for discrete-time switched nonlinear systems, the global exponential stability is found to be equivalent to the existence of an $M$ -step sequence with sufficient length and a family of Lyapunov functions, and then a stability criterion is proposed for the nominal linear case in the framework of quadratic Lyapunov function. In order to extend the stability criterion to handle uncertainties, an equivalent condition which has a promising feature that is convex in system matrices is derived, leading to a robust stability criterion for uncertain discrete-time switched linear systems. Moreover, also taking the advantage of the convex feature, the disturbance attenuation performance in the sense of $\ell _2$ -gain is studied. Several numerical examples are provided to illustrate our approach.

This paper addresses the output reachable set estimation problem for continuous-time switched linear systems consisting of Hurwtiz stable subsystems. Based on a common Lyapunov function approach, the output reachable set is estimated by a union of bounding ellipsoids. Then, multiple Lyapunov functions with time-scheduled structure are employed to estimate the output reachable set for switched systems under dwell-time constraint. Furthermore, the safety verification problem of uncertain switched systems is investigated based on the result of output reachable set estimation. First, a sufficient condition ensuring the existence of an approximate bisimulation relation between two switched linear systems with a prescribed precision is proposed. Then, the safety verification for an uncertain switched system can be performed through an alternative safety verification for a switched system with exact parameters. Numerical examples are provided to illustrate our results.

In this paper, we present virtual prototyping of the distributed control for a modular multilevel inverter used as a grid-tie interface for photovoltaics. Due to the distributed control and inherent redundancy in the system composed of many panels and inverter modules, the system topology exhibits fault-tolerance capabilities that we study through virtual prototyping. The fault-tolerance is enabled by several distributed algorithms, such as services to identify which, if any, agents controlling inverter modules have failed. A distributed identifier algorithm allows the system to keep track of the number of operating panels to appropriately regulate the dc voltage output of the panels using buck-boost converters and determine appropriate switching times for H-bridges in the grid-tie. We evaluate the distributed inverter, its control strategy, and fault-tolerance through thousands of simulation scenarios in Mathworks Simulink/Stateflow. Our virtual prototyping framework allows for generating multilevel inverters composed of many inverter modules, and we evaluate inverters composed of five to dozens of inverter modules. Our analysis suggests the achievable total harmonic distortion of the modular multilevel inverter may allow for operating solar arrays in spite of failures of the power electronics, control software, and other subcomponents.