Experiences from Large-Scale Model Checking: Verification of a Vehicle Control System
This work provides insights for architects, developers, and test engineers involved in verifying complex vehicle control systems, offering an incremental step in applying formal verification to a real-world, safety-critical domain.
This paper applies model checking to verify the arbitration logic of a Vehicle Control System, resulting in a model of approximately 1500 lines of code, 69 state variables, and 38 LTL constraints. The authors automated and optimized the model checking procedure for multi-core CPUs and used Bounded Model Checking to address the state explosion problem.
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.