| 模型检验中抽象技术研究综述 |
| |
| 引用本文： | 屈婉霞,李暾,郭阳,杨晓东.模型检验中抽象技术研究综述[J].计算机工程与应用,2006,42(33):15-19. |
| |
| 作者姓名： | 屈婉霞 李暾 郭阳 杨晓东 |
| |
| 作者单位： | 国防科学技术大学,计算机学院,长沙,410073 |
| |
| 摘 要： | 在模型检验中,抽象技术是解决状态空间爆炸问题的有效方法之一。论文描述了模型检验对抽象模型的基本要求,给出了抽象模型的定义及其评价指标,对抽象技术和自动化的抽象精化技术的主要方法及其研究进展作了比较深入、全面的综述,并讨论了抽象技术今后的发展方向。
|
| 关 键 词： | 模型检验 谓词抽象 抽象精化 反例 插值 |
| 文章编号： | 1002-8331（2006）33-0015-05 |
| 收稿时间： | 2006-09 |
| 修稿时间： | 2006-09 |
Survey of Abstraction Technologies for Model Checking |
| |
| QU Wan-xia,LI Tun,GUO Yang,YANG Xiao-dong.Survey of Abstraction Technologies for Model Checking[J].Computer Engineering and Applications,2006,42(33):15-19. |
| |
| Authors: | QU Wan-xia LI Tun GUO Yang YANG Xiao-dong |
| |
| Affiliation: | Department of Computer Science and Technology,National University of Defense Technology, Changsha 410073, China |
| |
| Abstract: | Abstraction is one of the most effective way to handle state explosion in model checking.This paper describes the requirements for abstract model.Definition and evaluation metrics of abstract model are also presented. Recent advances in abstraction, especially predicate abstraction,and automatic abstraction-refinement are analyzed in detaiI.Finally,a discussion is given to probe into the development perspective of abstraction techniques. |
| |
| Keywords: | model checking predicate abstraction abstraction/refinement counterexample interpolant |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
