Experiences from Large-Scale Model Checking: Verification of a Vehicle Control System

TL;DR

This paper discusses applying large-scale model checking to verify a vehicle control system's arbitration logic, highlighting challenges, techniques, and lessons learned to improve safety verification in autonomous vehicles.

Contribution

It presents practical experiences, modeling approaches, and optimization strategies for large-scale model checking of complex embedded systems in autonomous vehicles.

Findings

Successful verification of a complex vehicle control system model

Use of Bounded Model Checking to manage state explosion

Insights into modeling and tool selection for large-scale systems

Abstract

In the age of autonomously driving vehicles, functionality and complexity of embedded systems are increasing tremendously. Safety aspects become more important and require such systems to operate with the highest possible level of fault tolerance. Simulation and systematic testing techniques have reached their limits in this regard. Here, formal verification as a long established technique can be an appropriate complement. However, the necessary preparatory work like adequately modeling a system and specifying properties in temporal logic are anything but trivial. In this paper, we report on our experiences applying model checking to verify the arbitration logic of a Vehicle Control System. We balance pros and cons of different model checking techniques and tools, and reason about our choice of the symbolic model checker NuSMV. We describe the process of modeling the architecture, resulting in ~1500 LOC, 69 state variables and 38 LTL constraints. To handle this large-scale model, we automate and optimize the model checking procedure for use on multi-core CPUs and employ Bounded Model Checking to avoid the state explosion problem. We share our lessons learned and provide valuable insights for architects, developers, and test engineers involved in this highly present topic.