计算机工程与应用 ›› 2006, Vol. 42 ›› Issue (33): 15-19.
• 博士论坛 • 上一篇
屈婉霞,李暾,郭阳,杨晓东
收稿日期:
修回日期:
出版日期:
发布日期:
通讯作者:
,,,
Received:
Revised:
Online:
Published:
摘要： 在模型检验中，抽象技术是解决状态空间爆炸问题的有效方法之一。本文描述了模型检验对抽象模型的基本要求，给出了抽象模型的定义及其评价指标，对抽象技术和自动化的抽象求精技术的主要方法及其研究进展作了比较深入、全面的综述，并指出了抽象技术今后的发展方向。
关键词: 模型检验, 谓词抽象, 抽象精化, 反例, 插值
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 detail . Finally, a discussion is given to probe into the development perspective of abstraction techniques.
Key words: model checking, predicate abstraction, abstraction refinement, counterexample, interpolant
屈婉霞,李暾,郭阳,杨晓东. 模型检验中抽象技术研究综述[J]. 计算机工程与应用, 2006, 42(33): 15-19.
,,,. A Survey of Abstraction Technologies for Model Checking[J]. Computer Engineering and Applications, 2006, 42(33): 15-19.
0 / 推荐
导出引用管理器 EndNote|Ris|BibTeX
链接本文: http://cea.ceaj.org/CN/
http://cea.ceaj.org/CN/Y2006/V42/I33/15
