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

作     者：叶俊民 谢茜 金聪 李明 张振方 YE Jun-min;XEI Qian;JIN Cong;LI Ming;ZHANG Zhen-fang

作者机构：华中师范大学计算机科学系武汉430079 

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

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2010年第37卷第5期

页      码：118-122,174页

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

主 题 词：模型检验 程序分析 自动NuSMV输入工具 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1002-137X.2010.05.028

馆 藏 号：203641314...