摘要： 为提高程序编写的正确率，减少软件开发和维护开销，提出一种基于错误模式和模型检验的静态代码分析方法。该方法将C语言程序常见的错误模式以CTL公式表示，形成可扩展的CTL公式库，生成待检测程序的控制流图(CFG)后，将CFG抽象并转化为等价的 Kripke结构，利用标号算法实现模型检验，由此验证程序的正确性。基于CoSy编译平台的实验结果表明，该方法能正确查找出程序中存在的错误模式，且具有良好的可扩展性。
关键词:
错误模式,
模型检验,
CTL公式,
控制流图,
Kripke结构,
CoSy编译器平台
Abstract: 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.
Key words:
fault mode,
model check,
CTL formula,
Control Flow Graph(CFG),
Kripke structure,
CoSy complier platform
中图分类号:
魏雪菲, 吴健, 阮园. 基于错误模式和模型检验的静态代码分析方法[J]. 计算机工程, 2012, 38(06): 47-49.
WEI Xue-Fei, TUN Jian, RUAN Wan. Static Code Analysis Method Based on Fault Mode and Model Check[J]. Computer Engineering, 2012, 38(06): 47-49.