James Kapinski

Autonomous vehicles are complex systems that are challenging to test and debug. A requirements-driven approach to the development process can decrease the resources required to design and test these systems, while simultaneously increasing the reliability. We present a testing framework that uses signal temporal logic (STL), which is a precise and unambiguous requirements language. Our framework evaluates test cases against the STL formulae and additionally uses the requirements to automatically identify cases that fail to satisfy the requirements. One of the key features of our tool is the support for machine learning (ML) components in the system design, such as deep neural networks. Our framework includes evaluation of the control algorithms, including the ML components, and it also includes models of CCD camera, lidar, and radar sensors, as well as the vehicle environment. We use multiple methods to generate test cases, including covering arrays, which is an efficient method to search discrete variable spaces.The resulting test cases can be used to debug the controller design by identifying controller behaviors that do not satisfy requirements. The test cases can also enhance the testing phase of development by identifying critical corner cases that correspond to the limits of the system's allowed behaviors.

There is recent interest in using deep neural networks (DNNs) for controlling autonomous cyber-physical systems (CPSs). One challenge with this approach is that many autonomous CPS applications are safety-critical, and is not clear if DNNs can proffer safe system behaviors. To address this problem, we present an approach to modify existing (deep) reinforcement learning algorithms to guide the training of those controllers so that the overall system is safe. We present a novel verification-in-the-loop training algorithm that uses the formalism of barrier certificates to synthesize DNN-controllers that are safe by design. We demonstrate a proof-of-concept evaluation of our technique on multiple CPS examples.

Evaluation of industrial embedded control system designs is a time-consuming and imperfect process. While an ideal process would apply a formal verification technique such as model checking or theorem proving, these techniques do not scale to industrial design problems, and it is often difficult to use these techniques to verify performance aspects of control system designs, such as stability or convergence. For industrial designs, engineers rely on testing processes to identify critical or unexpected behaviors. We propose a novel framework called Underminer to improve the testing process; this is an automated technique to identify nonconverging behaviors in embedded control system designs. Underminer treats the system as a black box and lets the designer indicate the model parameters, inputs, and outputs that are of interest. It differentiates convergent from nonconvergent behaviors using Convergence Classifier Functions (CCFs). The tool can be applied in the context of testing models created late in the controller development stage, where it assumes that the given model displays mostly convergent behavior and learns a CCF in an unsupervised fashion from such convergent model behaviors. This CCF is then used to guide a thorough exploration of the model with the help of optimization-guided techniques or adaptive sampling techniques, with the goal of identifying rare nonconvergent model behaviors. Underminer can also be used early in the development stage, where models may have some significant nonconvergent behaviors. Here, the framework permits designers to indicate their mental model for convergence by labeling behaviors as convergent/nonconvergent and then constructs a CCF using a supervised learning technique. In this use case, the goal is to use the CCF to test an improved design for the model. Underminer supports a number of convergence-like notions, such as those based on Lyapunov analysis and temporal logic, and also CCFs learned directly from labeled output behaviors using machine-learning techniques such as support vector machines and neural networks. We demonstrate the efficacy of Underminer by evaluating its performance on several academic as well as industrial examples.

The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid sys- tems; however, state-of-the-art theorem provers require ex- tensive manual intervention. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assis- tance that a system designer is able to provide. This paper presents an extension to KeYmaera, a deductive verification tool for differential dynamic logic; the new technique allows local reasoning using system designer intuition about per- formance within particular modes as part of a proof task. Our approach allows the theorem prover to leverage for- ward invariants, discovered using numerical techniques, as part of a proof of safety. We introduce a new inference rule into the proof calculus of KeYmaera, the forward invariant cut rule, and we present a methodology to discover useful forward invariants, which are then used with the new cut rule to complete verification tasks. We demonstrate how our new approach can be used to complete verification tasks that lie out of the reach of existing deductive approaches us- ing several examples, including one involving an automotive powertrain control system.

We present a search technique to falsify safety properties of hybrid systems that model a software system controlling a physical plant. Our approach takes as input (a) the controller code and (b) a plant model given as a black-box system that can be simulated for given inputs over finite time horizons. Our approach combines the symbolic execution of the controller software with an abstraction of the plant, which is discovered on-the-fly using simulations. This process is used to find abstract counterexamples to the safety properties of interest. The plant abstraction is then refined iteratively using the abstract counterexamples until a concrete violation is discovered. Empirical evaluation of our approach shows its promise in treating controller software, whose semantics are well-understood using formal techniques while using numerical simulations to produce abstractions of the underlying plant model, which is often an approximation of the actual plant.

In Model-Based Design of Cyber-Physical Systems (CPS), it is often desirable to develop several models of varying fidelity. Models of different fidelity levels can enable mathematical analysis of the model, control synthesis, faster simulation etc. Furthermore, when (automatically or manually) transitioning from a model to its implementation on an actual computational platform, then again two different versions of the same system are being developed. In all previous cases, it is necessary to define a rigorous notion of conformance between different models and between models and their implementations. This paper argues that conformance should be a measure of distance between systems. Albeit a range of theoretical distance notions exists, a way to compute such distances for industrial size systems and models has not been proposed yet. This paper addresses exactly this problem. A universal notion of conformance as closeness between systems is rigorously defined, and evidence is presented that this implies a number of other application-dependent conformance notions. An algorithm for detecting that two systems are not conformant is then proposed, which uses existing proven tools. A method is also proposed to measure the degree of conformance between two systems. The results are demonstrated on a range of models.