基于错误模式和模型检验的静态代码分析方法

摘要：

为提高程序编写的正确率,减少软件开发和维护开销,提出一种基于错误模式和模型检验的静态代码分析方法.该方法将C语言程序常见的错误模式以CTL公式表示,形成可扩展的CTL公式库,生成待检测程序的控制流图(CFG)后,将CFG抽象并转化为等价的Kripke结构,利用标号算法实现模型检验,由此验证程序的正确性.基于CoSy编译平台的实验结果表明,该方法能正确查找出程序中存在的错误模式,且具有良好的可扩展性.

关键词：错误模式、模型检验、CTL公式、控制流图、Kripke结构、CoSy编译器平台

所属期刊栏目：38

分类号：TP391(计算技术、计算机技术)

资助基金：“核高基”重大专项“面向终端应用的高性能、低功耗嵌入式DSP”2009ZX0 1034-001-002-003

在线出版日期：2012-05-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：47-49