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

• 作者: 吴健 阮园 魏雪菲
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 错误模式 模型检验 CTL公式 控制流图 Kripke结构 CoSy编译器平台
• 年，卷（期）: 2012,（6）
• 所属期刊栏目: 软件技术与数据库
• 页码范围: 47-49
• 分类号: TP391
• 字数: 3569字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2012.06.015

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吴健	西北工业大学计算机学院	120	966	17.0	23.0
2	魏雪菲	西北工业大学计算机学院	1	5	1.0	1.0
3	阮园	中国电子科技集团公司第五十八研究所	12	47	4.0	6.0