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.
翻译:在自动驾驶车辆的时代,嵌入系统的功能和复杂性正在急剧增加。安全方面变得日益重要,要求这些系统以尽可能高的防故障度运作。模拟和系统测试技术已经达到了极限。在这里,正式核查作为一种长期确立的技术可以是一个适当的补充。然而,必要的准备工作,例如适当建模一个系统和用时间逻辑来说明特性等,只是微不足道而已。在本文件中,我们报告了我们应用示范检查来核查车辆控制系统的仲裁逻辑的经验。我们平衡了不同模式检查技术和工具的利弊,并说明了我们选择象征性的NusMV检查器的理由。我们描述了建筑模型的模型过程,结果产生了~1500 LOC、69个状态变量和38 LTL的限制。为了处理这一大型模型,我们自动化和优化模型检查程序,以便在多核心CPU上使用,并采用Bounded模型检查以避免国家爆炸问题。我们分享我们的经验教训,并向参与这个高度主题的建筑师、开发商和测试工程师提供宝贵的见解。