计算机科学 ›› 2010, Vol. 37 ›› Issue (5): 118-122174.
• 软件工程 • 上一篇 下一篇
叶俊民，谢茜，金聪，李明，张振方
出版日期:
发布日期:
基金资助:
YE Jun-min,XIE Qian,JIN Cong,LI Ming,ZHANG Zhen-fang
Online:
Published:
摘要： 提出了一种用模型检验技术对程序进行分析的方法，其主要思想是将C/C++源代码转换为与控制流图等价的Kripke结构，用CTL公式描述待验证的源程序性质，使用NuSMV模型检验工具实施具体的程序分析。基于这一思想，设计并实现了一个自动将C/C+ }源代码转换为NuSMV输入的工具。所做的实验验证表明，该方法能够有效地对程序进行分析。
关键词: 模型检验，程序分析，自动NuSMV输入工具
Abstract: A model checking-based program analysis method was proposed. The main steps include translating C/C++ source code into Kripke structure that is equivalent to control flow graph, describing properties of source code in CTL formula and verifying the program using model checker NuSMV. Based on this idea, a tool which is used to automatically translate C/C++ source code into NuSMV input was designed and implemented. The experiments show that this approach is able to analyze the program effectively.
Key words: Model checking, Program analysis,Automatic NuSMV input tool
叶俊民，谢茜，金聪，李明，张振方. 一种基于模型检验程序分析技术的前端工具研究[J]. 计算机科学, 2010, 37(5): 118-122174. https://doi.org/
YE Jun-min,XIE Qian,JIN Cong,LI Ming,ZHANG Zhen-fang. Research on a Front-end Tool for Program Analysis Based on Model Checking[J]. Computer Science, 2010, 37(5): 118-122174. https://doi.org/
0 / / 推荐
导出引用管理器 EndNote|Reference Manager|ProCite|BibTeX|RefWorks
链接本文: https://www.jsjkx.com/CN/
https://www.jsjkx.com/CN/Y2010/V37/I5/118
Cited
首页