An approach for formally verifying the safety of automated vehicles is proposed. Due to the uniqueness of each traffic situation, we verify safety online, i.e., during the operation of the vehicle. The verification is performed by predicting the set of all possible occupancies of the automated vehicle and other traffic participants on the road. In order to capture all possible future scenarios, we apply reachability analysis to consider all possible behaviors of mathematical models considering uncertain inputs (e.g., sensor noise, disturbances) and partially unknown initial states. Safety is guaranteed with respect to the modeled uncertainties and behaviors if the occupancy of the automated vehicle does not intersect that of other traffic participants for all times. The applicability of the approach is demonstrated by test drives with an automated vehicle at the Robotics Institute at Carnegie Mellon University.

The safety of the planned paths of autonomous cars with respect to the movement of other traffic participants is considered. Therefore, the stochastic occupancy of the road by other vehicles is predicted. The prediction considers uncertainties originating from the measurements and the possible behaviors of other traffic participants. In addition, the interaction of traffic participants, as well as the limitation of driving maneuvers due to the road geometry, is considered. The result of the presented approach is the probability of a crash for a specific trajectory of the autonomous car. The presented approach is efficient as most of the intensive computations are performed offline, which results in a lean online algorithm for real-time application.

Given an initial set of a nonlinear system with uncertain parameters and inputs, the set of states that can possibly be reached is computed. The approach is based on local linearizations of the nonlinear system, while linearization errors are considered by Lagrange remainders. These errors are added as uncertain inputs, such that the reachable set of the locally linearized system encloses the one of the original system. The linearization error is controlled by splitting of reachable sets. Reachable sets are represented by zonotopes, allowing an efficient computation in relatively high-dimensional space.

The probabilistic prediction of road traffic scenarios is addressed. One result is a probabilistic occupancy of traffic participants, and the other result is the collision risk for autonomous vehicles when executing a planned maneuver. The probabilistic occupancy of surrounding traffic participants helps to plan the maneuver of an autonomous vehicle, whereas the computed collision risk helps to decide if a planned maneuver should be executed. Two methods for the probabilistic prediction are presented and compared: 1) Markov chain abstraction and 2) Monte Carlo simulation. The performance of both methods is evaluated with respect to the prediction of the probabilistic occupancy and the collision risk. For each comparison test, we use the same models that generate the probabilistic behavior of traffic participants, where the generation of these data is not compared with real-world data. However, the results independently show the behavior generation that Markov chains are preferred for the probabilistic occupancy, whereas Monte Carlo simulation is clearly preferred for determining the collision risk.