Exploiting Formal Verification for the Systematic Discovery of Corner Cases in a Behavior Planner for Automated Driving

In automated driving, preventing hazardous driving decisions is both an extremely important and intricate task. Typical verification and validation methods include extensive simulation and real-world testing which is expensive and, yet, cannot rule out rare but potentially hazardous corner cases. Therefore, we present an approach to enhance the verification and validation process of automated driving by applying formal verification techniques for bug finding directly to the code of a tactical behavior planner in series development. We use an open source software framework in combination with the model checker nuXmv. Our framework involves fully automatically extracting the model from C++ code, integrating it with a traffic simulator, and conducting exhaustive analysis over a broad range of possible traffic scenes using model checking. If violations, e. g., crashes, are detected, traces of the surrounding traffic participants and ego are obtained, which can be simulated with the full system to aid in error identification, or utilized to generate corner cases for conventional testing. Since model checking is usually runtime-intensive, we analyze the effects of different discretization step sizes for time and space. Our results show that the toolchain identifies formerly unknown bugs in a real series development, even with surprisingly coarse discretizations. This demonstrates that model checking can improve the development process of industrial ADAS projects.