Experiences from Large-Scale Model Checking: Verification of a Vehicle Control System.
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 often reach 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.
Wed 14 AprDisplayed time zone: Brasilia, Distrito Federal, Brazil change
14:00 - 16:00 | |||
14:00 30mPaper | Industrial-Scale Passive Testing with T-EARS. Industry Track Daniel Flemström , Henrik Jonsson , Eduard Paul Enoiu Mälardalen University, Wasif Afzal Mälardalen University | ||
14:30 30mPaper | Boosting Exploratory Testing of Industrial Automation Systems with AI. Industry Track | ||
15:00 30mPaper | Experiences from Large-Scale Model Checking: Verification of a Vehicle Control System. Industry Track Jonas Fritzsch University of Stuttgart, Institute of Software Engineering, Tobias Schmid , Stefan Wagner University of Stuttgart Pre-print | ||
15:30 30mPaper | Digital Twins Are Not Monozygotic - Comparing ADAS Testing in Two Industry-Grade Automotive Simulators. Industry Track Markus Borg RISE Research Institutes of Sweden, Raja Ben Abdessalem , Shiva Nejati University of Ottawa, Canada / University of Luxembourg, Luxembourg, Francois-Xavier Jegeden , Donghwan Shin University of Luxembourg |