Successful Use of Incremental BMC in the Automotive Industry
Successful Use of Incremental BMC in the Automotive Industry
复制标题
增量式BMC在汽车行业的成功应用
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Tom Bienmüller
中科院分区：
文献类型：
--
作者：
P. Schrammel;D. Kroening;M. Brain;R. Martins;Tino Teige;Tom Bienmüller
在嵌入式系统开发中，程序分析即将成为主流应用。行为需求的形式化验证、发现运行时错误和自动测试用例生成是基于有界模型检测(BMC)的自动化验证工具的一些最常见的应用。现有的嵌入式软件工业工具使用现成的有界模型检查器，并迭代地应用它来验证程序，展开的次数越来越多。这种方法不必要地浪费时间，重复已经完成的工作，并且无法利用增量SAT求解的能力。本文介绍了对软件模型检查器CBMC的扩展，使其支持增量BMC，并与工业嵌入式软件验证工具BTC EmbeddedTester成功集成。我们对主要来自汽车行业的大型工业嵌入式程序进行了广泛的评估。我们表明，与标准的非增量方法相比，增量BMC将运行时间缩短了一个数量级，从而使形式验证能够应用于大型和复杂的嵌入式软件。
Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and automated test case generation are some of the most common applications of automated verification tools based on Bounded Model Checking (BMC). Existing industrial tools for embedded software use an off-the-shelf Bounded Model Checker and apply it iteratively to verify the program with an increasing number of unwindings. This approach unnecessarily wastes time repeating work that has already been done and fails to exploit the power of incremental SAT solving. This paper reports on the extension of the software model checker Cbmc to support incremental BMC and its successful integration with the industrial embedded software verification tool BTC EmbeddedTester. We present an extensive evaluation over large industrial embedded programs, mainly from automotive industry. We show that incremental BMC cuts runtimes by one order of magnitude in comparison to the standard non-incremental approach, enabling the application of formal verification to large and complex embedded software.
使用 SMT 求解对离散时间 MATLAB/Simulink 模型进行位精确形式验证
DOI：
10.1109/emsoft.2013.6658586
发表时间：
2013
期刊：
2013 Proceedings of the International Conference on Embedded Software (EMSOFT)
影响因子：
--
作者：
Paula Herber;Robert Reicherdt;Patrick Bittner
通讯作者：
Patrick Bittner