Search

We present an overview of recently developed data-driven tools for safety analysis of autonomous vehicles and advanced driver assist systems. The core algorithms combine model-based, hybrid system reachability analysis with sensitivity analysis of components with unknown or inaccessible models. We illustrate the applicability of this approach with a new case study of emergency braking systems in scenarios with two or three vehicles. This problem is representative of the most common type of rear-end crashes, which is relevant for safety analysis of automatic emergency braking (AEB) and forward collision avoidance systems. We show that our verification tool can effectively prove the safety of certain scenarios (specified by several parameters like braking profiles, initial velocities, uncertainties in position and reaction times), and also compute the severity of accidents for unsafe scenarios. Through hundreds of verification experiments, we quantified the safety envelope of the system across relevant parameters. These results show that the approach is promising for design, debugging and certification. We also show how the reachability analysis can be combined with statistical information about the parameters, to assess the risk level of the control system, which in turn is essential, for example, for determining Automotive Safety Integrity Levels (ASIL) for the ISO26262 standard., Comment: 7 pages, 5 figures, under submission to IEEE Design & Test

We present the DRYVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the learned sensitivity, and (c) reasoning techniques based on simulation relations and sequential composition, that enable verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under shorter sequences. We demonstrate the utility of the framework by verifying a suite of automotive benchmarks that include powertrain control, automatic transmission, and several autonomous and ADAS features like automatic emergency braking, lane-merge, and auto-passing controllers., Comment: 25 pages, 3 figures