计算机工程2012，Vol.38Issue(6)：47-49,3.DOI:10.3969/j.issn.1000-3428.2012.06.015
基于错误模式和模型检验的静态代码分析方法
Static Code Analysis Method Based on Fault Mode and Model Check
摘要
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.关键词
错误模式/模型检验/CTL公式/控制流图/Kripke结构/CoSy编译器平台Key words
fault mode/ model check/ CTL formula/ Control Flow Graph(CFG)/ Kripke structure/ CoSy complier platform分类
信息技术与安全科学引用本文复制引用
魏雪菲,吴健,阮园..基于错误模式和模型检验的静态代码分析方法[J].计算机工程,2012,38(6):47-49,3.基金项目
“核高基”重大专项“面向终端应用的高性能、低功耗嵌入式DSP”(2009ZX0 1034-001-002-003) （2009ZX0 1034-001-002-003）
