节点文献

基于模型检验技术的源程序分析研究

Research on Model Checking Based Source Code Analysis

推荐 CAJ下载
PDF下载
不支持迅雷等下载工具，请取消加速工具后下载。

【Author】 YE Jun-min,ZHANG Zhen-fang,WANG Jing-hua,LI Rong(Department of Computer Science,Central China Normal University,Wuhan 430079,China)

【机构】华中师范大学计算机科学系；

【摘要】提出并实现了一种基于模型检验的源程序分析方法.该方法的主要步骤是将C/C++源代码转换为与控制流图等价的Kripke结构,用CTL公式描述源程序待验证的性质,通过使用NuSMV模型检验工具实施对源程序分析.实验验证表明,该方法能够给实现对源程序分析的目标.更多还原

【Abstract】 A model checking-based source code analysis method is proposed and implemented in this paper. 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 source code using model checker NuSMV. The experiments show that this approach is able to achieve the goal of source code analysis.更多还原

【关键词】模型检验；源程序分析；软件故障；
【Key words】 model checking； source code analysis； software fault；

【会议录名称】 2009年全国开放式分布与并行计算机学术会议论文集(上册)

【会议名称】2009年全国开放式分布与并行计算机学术会议

【会议时间】2009-09-26
【会议地点】中国新疆乌鲁木齐
【分类号】TP311.52

【主办单位】中国计算机学会开放系统专业委员会

知网节下载

节点文献中：

本文链接的文献网络图示:

本文的引文网络

节点文献