一种基于模型检验程序分析技术的前端工具研究

摘要：

提出了一种用模型检验技术对程序进行分析的方法,其主要思想是将C/C++源代码转换为与控制流图等价的Kripke结构,用CTL公式描述待验证的源程序性质,使用NuSMV模型检验工具实施具体的程序分析.基于这一思想,设计并实现了一个自动将C/C++源代码转换为NuSMV输入的工具.所做的实验验证表明,该方法能够有效地对程序进行分析.

关键词：模型检验、程序分析、自动NuSMV输入工具

所属期刊栏目：37

分类号：TP311(计算技术、计算机技术)

资助基金：武汉大学计算机软件工程国家重点实验室开放基金项目SKLSE20080705;湖北省自然科学基金2008CDB349;华中师范大学校基金2009A12;华中师范大学中央高校基本科研业务费项目CC-NU09Y01009和CCNU09Y01013

在线出版日期：2010-06-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：118-122,174