论文标题
在汽车代码上进行基准测试软件模型检查器
Benchmarking Software Model Checkers on Automotive Code
论文作者
论文摘要
本文报告了我们通过最先进的开源软件模型检查器验证汽车C代码的经验。嵌入式C代码是由Simulink开环控制器模型自动生成的。它的各种功能（决策逻辑，浮点和指针算术，费率限制器和状态流系统）以及浮点变量的广泛使用使验证代码高度挑战。我们的研究揭示了覆盖范围的巨大差异 - 与主要年度软件验证竞赛的结果相比，这最多仅占所有需求的20％ - 和工具强度。具有$ k $感应的验证者CBMC的手工制作的简单扩展可为63％的需求提供结果，而专有的BTC嵌入式嵌入式估计占80％，并获得了大多数其余要求的有限验证结果。
This paper reports on our experiences with verifying automotive C code by state-of-the-art open source software model checkers. The embedded C code is automatically generated from Simulink open-loop controller models. Its diverse features (decision logic, floating-point and pointer arithmetic, rate limiters and state-flow systems) and the extensive use of floating-point variables make verifying the code highly challenging. Our study reveals large discrepancies in coverage - which is at most only 20% of all requirements --- and tool strength compared to results from the main annual software verification competition. A hand-crafted, simple extension of the verifier CBMC with $k$-induction delivers results on 63% of the requirements while the proprietary BTC EmbeddedValidator covers 80% and obtains bounded verification results for most of the remaining requirements.
