The UnCoVerCPS Verification Approach to Automated Driving

Abstract

There are several benefits for bringing automated vehicles to the road: Possible reduction of traffic accidents, improvement of work life balance and social inclusion of aged or disabled persons, to name just a few. A significant challenge is the validation and verification of automated driving. Classical offline verification approaches require enumeration and discretization of all relevant state variables in all possible driving situations, which results in a state space explosion. A promising approach is the use of online verification techniques pursued in UnCoVerCPS . The methods developed in UnCoVerCPS are generally 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 model. By exchanging and negotiating verified maneuver plans, the freedom of collisions and safe operation in general can be guaranteed for the situation at hand. The system design is tailored to make the complete system amenable to verification. An overview is given in fig. 1: The system is decomposed into three layers (green boxes), where each is fulfilling a contract, which guarantees correct operation under specific types of uncertainties. The combination of the three layers enables safe operation under disturbances, input- and parameter uncertainties, non-determinisms of the communication channel as well as nondeterminism of the decisions of cooperation partners. On the lowest layer is the physical vehicle, 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 “TTC”, which stabilizes the vehicle around a given set trajectory, while operating on noisy measurement data. Vehicle model and trajectory tracking controller are considered as a closed loop system by an offline analysis shown at the bottom of fig. 1 (steps 1.Modeling – 6.Verification), which computes bounds on state evolution of the physical system (rather than the model), for a finite set of atomic actions (maneuver database – “MDB”). During online execution, several maneuver planners “MP” assemble the guarantees of the pre-verified atomic actions and use conservative bounds on the environment perception to generate provably safe maneuvers. A timed-automaton (cooperative driving controller – “CDC”) controls negotiation of safe, cooperative maneuvers with other vehicles. It guarantees safe operation even under the assumption of message loss and delays, as well as non-deterministic planning times. This is achieved by prudent switching between cooperative, individual and failsafe maneuvers. In this paper we give an overview of the offline design process, which, besides classical development steps, involves (fig.1, step 4.) sampling possible vehicle actions, (5.) generating a reliable model by testing conformance between the actual physical system and a model with bounded uncertainties and (6.) verifying time in-variant constraints and admissible execution orders of the vehicle actions. Furthermore we focus on the online execution, where maneuver planners and the cooperative driving controller guarantee compliance to time varying constraints. Where “monolithic” verification schemes are hampered by the curse of dimensionality, our modular and layered approach of verifying lower-level, closed-loop subsystems offline and higher-level decision modules online provides formal safety guarantees for the overall system in a feasible manner.