面向源代码的软件模型检测及其实现  

Source-oriented Software Model Checking and its Implementation

作　　者：何恺铎[1,2] 顾明[1,2] 宋晓宇 李力[1,2] 李江[1] 

机构地区：[1]清华大学软件学院,北京100084 [2]清华大学计算机科学与技术系,北京100084 [3]Dept.ECE,Portl and State University

出　　处：《计算机科学》2009年第1期267-272,共6页Computer Science

基　　金：国家自然科学基金(No.60553002;No.90718039)支持

摘　　要：模型检测应用于检测软件可靠性具有重要意义。介绍了一种基于谓词抽象和反例引导抽象求精技术对源程序进行建模和验证的模型检测方法,并结合自行研发的Jchecker工具详细介绍了该软件模型检测技术的运作过程和关键算法。Model checking on software reliability is always considered meaningful. This paper studied theory and methodology on source code verification, utilizing predicate abstraction and counterexample-guided abstraction refinement. Detailed verification framework and its implementation of the self-designed Jchecker, a source-oriented software model checker, were also introduced.

关 键 词：软件模型检测 源程序验证 谓词抽象 抽象求精 面向源代码 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]