Computer Engineering and Applications ›› 2006, Vol. 42 ›› Issue (33): 15-19.

• 博士论坛 • Previous Articles    

A Survey of Abstraction Technologies for Model Checking

,,,   

  1. 国防科技大学计算机学院
  • Received:2006-08-25 Revised:1900-01-01 Online:2006-11-21 Published:2006-11-21

模型检验中抽象技术研究综述

屈婉霞,李暾,郭阳,杨晓东   

  1. 国防科技大学计算机学院
  • 通讯作者: 屈婉霞 wxqu2002 wxqu2002

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

摘要: 在模型检验中,抽象技术是解决状态空间爆炸问题的有效方法之一。本文描述了模型检验对抽象模型的基本要求,给出了抽象模型的定义及其评价指标,对抽象技术和自动化的抽象求精技术的主要方法及其研究进展作了比较深入、全面的综述,并指出了抽象技术今后的发展方向。

关键词: 模型检验, 谓词抽象, 抽象精化, 反例, 插值