Safe Cooperation of Automated Vehicles

A significant challenge in automated vehicle design is validation and verification. Purely test-based validation approaches can suffer from extremely high number of required test kilometers, as well as difficulties to transfer results to new driving situations. Classical offline verification approaches struggle to account for the high number of environmental variables and the mixture of continuous and discrete dynamics, which are apparent in the application. A promising approach investigated in the EU project UnCoVerCPS is the combination of online and offline verification as well as testing steps. The methods developed in UnCoVerCPS are applicable to many safety critical, cyber physical systems. As a specific use case, we investigate a system, which facilitates safe interactions of automated vehicles. Leveraging a formal proof on a validated vehicle dynamics model and by negotiating exclusive access to phase space regions via Car-to-Car communication, the freedom of collisions and safe operation in other respects are ascertained online and for the situation at hand. Our design is tailored to make the distributed system amenable to verification. Each individual vehicle has to guarantee certain time and space requirements, thus allowing to show safety of the vehicle group. Individual vehicle guarantees are constructed by subdividing a vehicle into the tree layers “physical vehicle”, “closed-loop control” and “decision making”. The physical vehicle is modeled as a set of nonlinear differential equations with bounded uncertain parameters and disturbances. The second layer is realized by a classical discrete time trajectory tracking controller, which stabilizes the vehicle around a given reference trajectory, while operating on state measurements that are also considered to be afflicted by bounded errors. The first validation step in the approach is to subject the vehicle to test drives targeting the two lower layers: Bounds on system parameters, disturbances and measurement errors are derived, which establish conformance between the mathematical vehicle model and each of the recorded time series. The validation step is independent from the control layer, the decision layer and the surrounding traffic situation. Coverage of the vehicle’s operable state space region, as well as admissible disturbance situations is required, (which can be achieved with relatively few test km). Based on the validated model, a subsequent offline verification step computes a set of reference trajectories, their admissible order of execution and bounds on control performance under consideration of the closed loop controller. Using reachability analysis for nonlinear dynamical systems, the computed bounds are formally sound and thus reliability of the second layer is established. Results are grouped in a so called Maneuver Database (MDB), which is made available to the decision layer. At the decision layer, an online verification module uses the MDB to determine at each time-step, which available actions are safe and compliant with the cooperation requirements. An action is proven to be safe by appending an emergency maneuver, which leads to a safe terminal state, adheres to precomputed bounds of the MDB and is collision free under certain types of worst-case behaviors of other traffic participants. Behavioral software components can be attached to the online verification module, e.g. behaviors for lane-following, lane-changing, cooperative lane-changing, etc. As long as these modules select only from the set of verified actions, they cannot infringe on the vehicle’s safety property. On the level of vehicle cooperation, a formal analysis of the negotiation protocol establishes correctness under arbitrary message delay and loss. A prototypical implementation of the system design is presented and analyzed in simulation for two cooperating vehicles. It remains to conclude with several benefits of our approach: Very limited physical testing is required. In contrast to other approaches, which are either restricted to linear systems or nonlinear systems in a small state space region, our approach is able to cover a broad operation regime for a nonlinear vehicle model and maintains guarantees for transitions between different areas of the state space. The offline analysis of the closed loop system and the precomputation of bounds enable formally sound online decision making. Furthermore, the online verification module is able to handle unforeseen traffic situations and encapsulates the safety property in such a way that computations of other behavioral modules cannot affect correctness