摘要
为提高程序编写的正确率,减少软件开发和维护开销,提出一种基于错误模式和模型检验的静态代码分析方法。该方法将C语言程序常见的错误模式以CTL公式表示,形成可扩展的CTL公式库,生成待检测程序的控制流图(CFG)后,将CFG抽象并转化为等价的Kripke结构,利用标号算法实现模型检验,由此验证程序的正确性。基于CoSy编译平台的实验结果表明,该方法能正确查找出程序中存在的错误模式,且具有良好的可扩展性。
In order to improve the procedure accuracy and reduce software development and maintenance costs, this paper proposes a static code analysis method based on fault mode and model check. Common C program fault modes are described as CTL formulas form, and an extendable CTL formula library is established. Control Flow Graph（CFG） is generated from testing procedure, and then converted into an equivalent Kripke structure. Labeling algorithm is used to realize model check, so that the procedure can be checked whether it is correct. Experiments based on CoSy compiler platform indicate that the method can correctly find out the fault modes in procedure with good scalability.
出处
《计算机工程》
CAS
CSCD
2012年第6期47-49,共3页
Computer Engineering
基金
"核高基"重大专项"面向终端应用的高性能
低功耗嵌入式DSP"(2009ZX01034-001-002-003)
