计算机工程 ›› 2012, Vol. 38 ›› Issue (06): 47-49.doi: 10.3969/j.issn.1000-3428.2012.06.015

• 软件技术与数据库 • 上一篇    下一篇

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

魏雪菲 1,吴 健 1,阮 园 2   

  1. (1. 西北工业大学计算机学院,西安 710072;2. 中国电子科技集团公司第五十八研究所,江苏 无锡 214035)
  • 收稿日期:2011-04-29 出版日期:2012-03-20 发布日期:2011-03-20
  • 作者简介:魏雪菲(1985-),女,硕士,主研方向:代码分析,软件工程;吴 健,教授;阮 园,高级工程师
  • 基金项目:
    “核高基”重大专项“面向终端应用的高性能、低功耗嵌入式DSP”(2009ZX01034-001-002-003)

Static Code Analysis Method Based on Fault Mode and Model Check

WEI Xue-fei 1, WU Jian 1, RUAN Yuan 2   

  1. (1. College of Computer, Northwestern Polytechnical University, Xi’an 710072, China; 2. No.58 Research Institute of China Electronics Technology Group Corporation, Wuxi 214035, China)
  • Received:2011-04-29 Online:2012-03-20 Published:2011-03-20

摘要: 为提高程序编写的正确率,减少软件开发和维护开销,提出一种基于错误模式和模型检验的静态代码分析方法。该方法将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

中图分类号: