|
|||||
|
|
| 面向源代码的软件模型检测及其实现 | |
| 引用本文： | 何恺铎,顾明,宋晓宇,李力,李江.面向源代码的软件模型检测及其实现[J].计算机科学,2009,36(1):267-272. |
| 作者姓名： | 何恺铎 顾明 宋晓宇 李力 李江 |
| 作者单位： | 1. 清华大学软件学院,北京,100084;清华大学计算机科学与技术系,北京,100084 2. Dept.ECE,Portland State University,Oregon,USA 3. 清华大学软件学院,北京,100084 |
| 摘 要： | 模型检测应用于检测软件可靠性具有重要意义.介绍了一种基于谓词抽象和反例引导抽象求精技术对源程序进行建模和验证的模型检测方法,并结合自行研发的Jchecker工具详细介绍了该软件模型检测技术的运作过程和关键算法. |
| 关 键 词： | 软件模型检测 源程序验证 谓词抽象 抽象求精 |
| 收稿时间： | 2008/2/22 0:00:00 |
Source-oriented Software Model Checking and its Implementation |
|
| HE Kai-duo,GU Ming,SONG Xiao-yu,LI Li,LI Jiang.Source-oriented Software Model Checking and its Implementation[J].Computer Science,2009,36(1):267-272. | |
| Authors: | HE Kai-duo GU Ming SONG Xiao-yu LI Li LI Jiang |
| Affiliation: | School of Software;Tsinghua University;Beijing 100084;China;Department of Computer Science and Technology;China;Dept.ECE;Portland State University;Oregon;USA |
| Abstract: | Model checking on software reliability is always considered meaningful.This paper studied theory and metho-dology 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. |
| Keywords: | Software model checking Source verification Predicate abstraction Abstraction refinement |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
| 点击此处可从《计算机科学》下载全文 | |
