软件模型检测中的抽象模型研究综述

来源：计算机研究与发展杂志2015年第7期北京时间：

作者：魏欧,石玉峰,徐丙凤,黄志球,陈哲,

摘要：抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为3类:1)传统的用于支持自上逼近或者自下逼近的布尔Kripke结构;2)分别对应于3值和4值Kripke结构的Kripke模态迁移系统(Kripkemodaltransitionsystems,KMTS)和混合迁移系统(mixedtransitionsystem,MixTS),可同时支持自上逼近和自下逼近的抽象;3)具有超迁移关系的广义Kripke模态迁移系统(generalizedKripkemodaltransitionsystem,GKMTS)和超迁移系统(hypertransitionsystem,HTS),可提供更精确的抽象模型检测;重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果.最后,分析了目前关于抽象模型的理论和应用研究中存在的问题,给出进一步研究的方向.

关键词：抽象模型, 自上逼近, 自下逼近, 模型检测, 多值模型,