Model checking C source code for embedded systems
Model checking C source code for embedded systems
复制标题
嵌入式系统的模型检查 C 源代码
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
S. Kowalewski
中科院分区：
文献类型：
--
作者：
Bastian Schlich;S. Kowalewski
在本文中，研究了模型检查对嵌入式系统的C代码的适用性。该纸分为两部分。在第一部分中，对C代码的13个现有模型检查器进行了详细介绍，并评估了其在嵌入式系统的C代码验证中的适用性。提出了一个案例研究，该案例将CBMC作为一个代表性C代码模型检查器应用于模范微控制器程序。由于本案例研究的结果，我们决定为微控制器的源代码开发一个新的模型检查器，称为[MC] Square。它在本文的第二部分中进行了描述。我们介绍了[MC]正方形的体系结构和特点，并成功地将[MC]正方形应用于案例研究中使用的同一微控制器程序。
In this paper, the applicability of model checking to C code for embedded systems is studied. The paper is divided into two parts. In the first part, 13 existing model checkers for C code are detailed and evaluated for their applicability in the verification of C code for embedded systems. A case study is presented that applied CBMC as one representative C code model checker to an exemplary microcontroller program. As a consequence of this case study, we decided to develop a new model checker for source code for microcontrollers, called [mc]square. It is described in the second part of this paper. We present the architecture and the peculiarities of [mc]square, and we successfully applied [mc]square to the same microcontroller program used in the case study.
DOI：
10.1007/978-3-642-28756-5_47
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Basler G
通讯作者：
Basler G