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

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.

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.

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.