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

摘要：

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

关键词： 模型检验 源程序分析 软件故障 控制流图

作者: 叶俊民 张振方 王敬华 李蓉

作者单位: 华中师范大学,计算机科学系,武汉,430079

会议类型: 国内会议

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

会议地点: 乌鲁木齐

会议语种:中文

页码: 166-170

在线出版日期: 2009-09-01（万方平台首次上网日期，不代表论文的发表时间）