Skip to main content
Research

Enhancing Trust in Autonomous Cars — Verification of Driving Capabilities using Model Checking

Bosch Research Blog | Posted by Christian Heinzemann and Michaela Klauck, 2024-05-13

Two Bosch researchers, Heinzemann Christian and Klauck Michaela, discussing the topic of Enhancing Trust in Autonomous Cars – Verification of Driving Capabilities using Model Checking in the Bosch Research Blog.

Automated driving functions need to make the right decisions in complex traffic situations. Bosch Research uses techniques based on math to prove that these decisions are always safe in all possible driving scenarios.

Do you trust the driving capabilities of autonomous cars? Imagine you’re driving on a highway and approaching a slow vehicle in front of you. You want to change lanes and overtake it, but faster cars are coming up from behind. Is it still safe to make the lane change? These are the kinds of questions we often have to answer while driving. If we rely on automated driving functions, the software needs to be able to answer these questions correctly in every possible traffic situation. Do you know how manufacturers currently ensure that accidents are avoided as much as possible?

Currently, trust is gained through thousands of kilometers of test drives, either in real-life or in simulations, where the car is exposed to all the driving scenarios it will encounter. We propose a different, rigorous solution based on mathematical calculations, which allows for a complete check of all possible driving scenarios in a specified road setup much earlier in the development process. This enables verification of (parts of) the car’s software with much lower costs and significantly less effort than testing, while still ensuring 100% reliability and coverage of corner cases.

In the automated driving alliance, Bosch’s Cross-Domain Computing Solutions (XC) division and CARIAD collaborate on developing automated driving functions ranging from level 2 hands-free systems for urban and highway driving to level 3 systems that take full control of the vehicle on highways. As the human driver is, at least partially, out of control with their hands off the steering wheel, the safety of these automated driving functions is of utmost importance. One of the core elements of such a function is a behavior planner that decides on the high-level actions to be taken based on the surrounding traffic. It is crucial that the decisions made by the behavior planner are safe and compliant with traffic rules in every possible traffic situation.

In a joint research activity between Bosch and the Fondazione Bruno Kessler, we asked ourselves if we could do even better than testing and find errors earlier in the development process with higher precision.

The Bosch researchers, Heinzemann Christian and Klauck Michaela during a work situation.

Our idea was to use formal methods from computer science to actually prove that (a part of) the software satisfies safety requirements. We particularly investigated a technique called model checking, which can be fully automated. One of the benefits of model checking is that it can identify system executions where the system fails to meet the requirements. These executions, known as counterexamples, can then be visualized and inspected by developers to make changes and improvements to the software accordingly.

A simplified illustration showcasing the process of model checking for a behavior planner.
A simplified illustration showcasing the process of model checking for a behavior planner.
Model checking
is a mathematical procedure used to verify that a system description satisfies a given specification, provided as a temporal formula reasoning over the temporal occurrence of events in the system. Checking whether the system fulfills the specification in all possible executions is a fully automatic procedure that requires no user interaction. The result is either a counterexample, which is a sequence of events in the system that violates the specification, or a statement that the system always satisfies the specification.

Our goal was to integrate model checking as seamlessly as possible into the engineers’ development process. This was achieved through two major parts in the toolchain we developed. First, the developer has minimal effort in using the model checker on the current version of the behavior planner. The required model is automatically extracted from the C++ code in which the planner is specified, with only a few annotations needed in the code. As Bosch Research, we mainly developed and contributed an environment model for the verification procedure, representing the road environment and the behavior of other cars in traffic situations. For the verification, we used the nuXmv model checker developed by the Fondazione Bruno Kessler. Their expertise in writing and designing the model for efficient model checking was crucial, as even small changes in the modeling procedure can greatly impact performance.

An animation of a driving scenario leading to an accident, discovered through model checking the behavior planner.
An animation of a driving scenario leading to an accident, discovered through model checking the behavior planner. The ego vehicle (red) only notices the car directly in front of it merging into its lane. When this car merges out and the second car in front of it brakes, the ego vehicle fails to detect it. The issue is caused by the ego vehicle not considering two vehicles attempting to merge at the same time and only considering the closer vehicle.

Second, the counterexamples provided by the model checker can be directly used by the developer in a feedback loop to make changes and improvements to the behavior planner, ensuring that violations of the specification found by the model checker are eliminated in future versions. The counterexamples are made easily understandable and interpretable to developers through the automatic generation of visualizations. With the automatic extraction of the behavior planner’s model from its C++ code, the integration of the nuXmv model checker, and the automatic generation of visualizations for behaviors that violate the checked specification, we were able to develop an efficient and user-friendly verification toolchain for behavior planners used in automated driving. This toolchain can be easily integrated into the development process and used by autonomous driving engineers without requiring knowledge of model checking.

The TACAS Distinguished Artifact Award at ETAPS

The Bosch researchers, Michaela Klauck and Christian Heinzemann with the TACAS Distinguished Artifact Award which they received at ETAPS 2024.
The Bosch researchers, Michaela Klauck and Christian Heinzemann, with the TACAS Distinguished Artifact Award which they received at ETAPS 2024.

We are honored to announce that our paper "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development" has been awarded the "TACAS Distinguished Artifact Award" at "ETAPS 2024", further highlighting the significance of our research.

This achievement is a testament to the collaborative efforts of Bosch Research, Fondazione Bruno Kessler, and CARIAD. We take immense pride in not only receiving recognition for providing an exceptional artifact with clear instructions on its usage but also for publishing a publicly accessible artifact as part of an industry paper.

If you're even more curious, check out our award-winning code artifact on Zenodo, where you can try out the full procedure yourself, starting from a behavior planner that violates specifications, model-checking it, and making changes to ensure its safety.

What are your thoughts on this topic?

Please feel free to share them or to contact us directly.

Christian Heinzemann is a senior expert for verification of autonomous systems at Bosch Corporate Research in the department “Advanced Digital and AI Solutions”.

Author: Christian Heinzemann

Christian is a senior expert for verification of autonomous systems at Bosch Corporate Research in the department “Advanced Digital and AI Solutions” in the cluster “Dependable Cyber-Physical Software Engineering”. He joined Bosch in 2015 working on verification of autonomous robots. Currently, Christian is leading a research activity working on the development of safe planning functions and on verification of planning and decision-making in automated driving functions. A key focus of his research is bringing formal methods and verification to industrial practice. Previously, Christian worked as a research associate at the University of Paderborn and at the Fraunhofer Institute for Mechatronic Systems Design (IEM). He holds a PhD in computer science from the University of Paderborn.

Michaela Klauck is a research engineer at Bosch Corporate Research in the department “Advanced Digital and AI Solutions” in the cluster “Dependable Cyber-Physical Software Engineering”.

Author: Michaela Klauck

Michaela is a research engineer at Bosch Corporate Research in the department “Advanced Digital and AI Solutions” in the cluster “Dependable Cyber-Physical Software Engineering”. Her focus lies in the verification of planning and decision making in autonomous systems. Since 2023, she has been working at Bosch on model-checking robotic deliberation and autonomous driving behavior. Currently, she is leading the CONVINCE activity in the Robotics Portfolio including an EU-funded project, where she is working on making autonomous robot behavior more robust using model checking techniques. Previously, she was a research associate at Saarland University, working in the area of quantitative verification, especially at the interface of these topics to automatic planning and the AI community. She holds a PhD in computer science. Thesis: “On the Connection of Probabilistic Model Checking, Planning, and Learning for System Verification”.

Share this on: