Advanced driver assistance system (ADAS) is effectively promoting the vehicular automation level and it is critical to ensure its functional safety. While existing analysis mainly focuses on individual applications of ADAS, safety violations in the overall system can be found by extensive road tests, which are not only costly in terms of time and money but also lack a formal safety guarantee. This is because tests may not cover all driving scenarios, especially the ones that involve discrete mode switching. In this paper, we focus on the longitudinal vehicle motion and provide a pipeline to perform safety verification for all the related ADAS applications. To that end, we specify safety constraints and boundaries for a vehicle's longitudinal cruising and collision avoidance and validate a longitudinal dynamic model against the high-fidelity simulation software CarSim. Then we define hybrid automata to describe the closed-loop system composed of the vehicle dynamics and the ADAS. Finally, by computing the reachable sets of the hybrid automata and comparing them with the specified safety boundaries, the ADAS is verified. Numerical experiments demonstrate the efficacy of the proposed approach.

In modern industry, human–robot collaboration is becoming the norm. Since the robots need to share the same workspace with humans in an unstructured/semistructured environment, robot–human and robot–environment collisions are inevitable in general. To reduce the harm caused by these collisions, it is necessary to detect them in real time so that actions can be taken accordingly. In this article, we propose a general robot collision detection method based on switched momentum dynamics identification. This enables real-time collision detection without any additional sensors, which are usually required by most of the existing real-time collision detection methods. Our algorithm identifies the specific parts in robot momentum dynamics that are affected by collisions and reports a collision occurrence whenever the identified parts deviate from a known collision-free model. The identification results are further analyzed using a support vector machine classifier to locate the linkage involved in the collisions. Finally, the effectiveness of our method is verified through experiments in the PyBullet environment and on a real 6-DOF robot, showing improved robustness to noise for identical collision detection accuracies.

Stable human movement is often defined as movement that does not lead to falling. The set of such movements is too broad to be encompassed by traditional notions of stability in control theory, such as stability about equilibria or trajectories. We propose framing the region of stable human movement, which we call the stabilizable region, as the backward reachable set of a controlled invariant set. We focus on sit-to-stand, which requires a high level of coordination and is a common setting for falls. Using tools from the hybrid systems community, we compute the stabilizable region for sit-to-stand under varying environmental and physiological conditions. We validate our results with a dataset of humans performing perturbed sit-to-stand.

Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This article is concerned with developing scalable algorithms that underapproximate the backward reachable sets, for discrete-time uncertain linear and nonlinear systems. Our algorithm sequentially linearizes the dynamics and uses constrained zonotopes for set representation and computation. The main technical ingredient of our algorithm is an efficient way to underapproximate the Minkowski difference between a constrained zonotopic minuend and a zonotopic subtrahend, which consists of all possible values of the uncertainties and the linearization error. This Minkowski difference needs to be represented as a constrained zonotope to enable subsequent computation, but, as we show, it is impossible to find a polynomial-size representation for it in polynomial time. Our algorithm finds a polynomial-size underapproximation in polynomial time. We further analyze the conservatism of this underapproximation technique and show that it is exact under some conditions. Based on the developed Minkowski difference technique, we detail two backward reachable set computation algorithms to control the linearization error and incorporate nonconvex state constraints. Several examples illustrate the effectiveness of our algorithms.

In this paper, we study feedback dynamical systems with memoryless controllers under imperfect information. We develop an algorithm that searches for “adversarial scenarios”, which can be thought of as the strategy for the adversary representing the noise and disturbances, that lead to safety violations. The main challenge is to analyze the closed-loop system's vulnerabilities with a potentially complex or even unknown controller in the loop. As opposed to commonly adopted approaches that treat the system under test as a black-box, we propose a synthesis-guided approach, which leverages the knowledge of a plant model at hand. This hence leads to a way to deal with gray-box systems (i.e., with known plant and unknown controller). Our approach reveals the role of the imperfect information in the violation. Examples show that our approach can find non-trivial scenarios that are difficult to expose by random simulations. This approach is further extended to incorporate model mismatch and to falsify vision-in-the-loop systems against finite-time reach-avoid specifications.

In this work, we consider detectability analysis for faults in systems governed by switched affine dynamics. By a fault, we mean a sudden and permanent change in the system dynamics. Given the model of the healthy system, such a fault can be detected via a model invalidation approach, i.e., by collecting historic observations over a finite horizon and checking whether these observations can be generated by the healthy system model. Whenever the faulty system model is also available, it is possible to find T, the minimum length of the horizon, with which the fault is guaranteed to be detected eventually (with a T-delay at most). The main contribution of this work is to show the possibility of reducing the value of T, by augmenting the fault detectability analysis with additional linear temporal logic (LTL) constraints on the switching signals, if any. We express the LTL constraints (restricted in a finite horizon) with a nondeterministic finite automaton (NFA), which is then transformed into a set of mixed integer linear constraints that can be easily integrated in the detectability analysis.

This paper employs correct-by-construction control synthesis, in particular controlled invariant set computations, for falsification. Our hypothesis is that if it is possible to compute a “large enough” controlled invariant set either for the actual system model or some simplification of the system model, interesting corner cases for other control designs can be generated by sampling initial conditions from the boundary of this controlled invariant set. Moreover, if falsifying trajectories for a given control design can be found through such sampling, then the controlled invariant set can be used as a supervisor to ensure safe operation of the control design under consideration. In addition to interesting initial conditions, which are mostly related to safety violations in transients, we use solutions from a dual game, a reachability game for the safety specification, to find falsifying inputs. We also propose optimization-based heuristics for input generation for cases when the state is outside the winning set of the dual game. To demonstrate the proposed ideas, we consider case studies from basic autonomous driving functionality, in particular, adaptive cruise control and lane keeping. We show how the proposed technique can be used to find interesting falsifying trajectories for classical control designs like proportional controllers, proportional integral controllers and model predictive controllers, as well as an open source real-world autonomous driving package.