A New Formal Verification Approach for Hardware-dependent Embedded System Software
A New Formal Verification Approach for Hardware-dependent Embedded System Software
复制标题
一种新的依赖于硬件的嵌入式系统软件形式化验证方法
DOI：
10.2197/ipsjtsldm.6.135
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
W. Kunz
中科院分区：
文献类型：
--
作者：
Bernard Schmidt;Carlos Villarraga;Thomas Fehmel;J. Bormann;Markus Wedler;Minh D. Nguyen;D. Stoffel;W. Kunz
本文描述了一种用于嵌入式系统中依赖硬件的软件形式化验证的计算模型的生成方法。组合的HW / SW系统的计算模型是由连接在有向非循环图中的指令单元组成的程序网表（PN），该有向非循环图compatible地表示软件的所有执行路径。该模型可以很容易地集成到基于SAT的验证环境中，例如基于Bounded Model Checking（BMC）的验证环境。该模型的建议建设允许一个有效的推理的SAT求解器在整个执行路径。程序网表是合成的。本文介绍了如何将它们结合起来，中断驱动的系统建模。我们证明了我们的方法的有效性，提出了实验结果，从正式验证的工业LIN（本地互连网络）总线节点，实现为一个软件驱动程序的32位RISC机器。
: This paper describes a method to generate a computational model for formal verification of hardware-dependent software in embedded systems. The computational model of the combined HW / SW system is a program netlist (PN) consisting of instruction cells connected in a directed acyclic graph that compactly represents all execution paths of the software. The model can be easily integrated into SAT-based verification environments such as those based on Bounded Model Checking (BMC). The proposed construction of the model allows for an e ffi cient reasoning of the SAT solver over entire execution paths. Program netlists are compositional. The paper presents how they can be combined to model interrupt-driven systems. We demonstrate the e ffi ciency of our approach by presenting experimental results from the formal verification of an industrial LIN (Local Interconnect Network) bus node, implemented as a software driver on a 32-bit RISC machine.