Motivation

The environment of an autonomous vehicle is complex and fast changing. The vehicles must cope with any traffic situation. Testing every situation is impossible, even clustering results in an impractical number of scenarios. However, classical verification, which is performed offline before a vehicle is launched, is infeasible because the environment is previously unknown.

Objective

The Goal of the project “Formal Methods for Active Trajectory Verification” in collaboration with Ford Motor Company, Michigan, USA, is to perform online verification using formal methods to manage uncertain future behaviors of traffic participants and disturbances acting on the host vehicle. Trajectories obtained from virtual driver typically using assumptions (e.g. the other vehicle continues with constant velocity). Those assumptions never hold in reality and thus obtained motion plans are not always safe. Since the uncertainty of possible behaviors of other traffic participants grows over time (indicated by the gray occupancy set), we apply our verification concept only to the first part of the long-term reference trajectories as depicted by the red path in Figure 1. The time horizon of this combined trajectory (first part of intended trajectory plus fail-safe trajectory) is short, such that the proposed set-based techniques do not block overly large regions for trajectory planning. The fail-safe trajectory brings the system into a safe state (e.g. standstill or safe distance behind another vehicle).

Let us now assume that the other vehicle is performing an unexpected maneuver as shown in the lower part of Figure 1. Consequently, Virtual Driver will plan a new optimal motion plan plus a new fail-safe trajectory. If the new combination of intended plan and fail-safe trajectory is verified as safe,we will follow it. However, it might be that due to the unexpected maneuver, we are not able to generate a new safe trajectory. In that event, we can follow the previously computed fail-safe trajectory, which has already been verified for all times. Since the previous fail-safe trajectory already considered all possible behaviors of the other traffic participant, it stays safe, even though the situation has changed.