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

Abstract Modeling Formalisms in Software Model Checking

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

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016 [2]南京林业大学信息科学技术学院,南京210037

出　　处：《计算机研究与发展》2015年第7期1580-1603,共24页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(61170043;61100034;61272083);国家"九七三"重点基础研究发展计划基金项目(2014CB744904)

摘　　要：抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为3类:1)传统的用于支持自上逼近或者自下逼近的布尔Kripke结构;2)分别对应于3值和4值Kripke结构的Kripke模态迁移系统(Kripke modal transition systems,KMTS)和混合迁移系统(mixed transition system,MixTS),可同时支持自上逼近和自下逼近的抽象;3)具有超迁移关系的广义Kripke模态迁移系统(generalized Kripke modal transition system,GKMTS)和超迁移系统(hyper transition system,HTS),可提供更精确的抽象模型检测;重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果.最后,分析了目前关于抽象模型的理论和应用研究中存在的问题,给出进一步研究的方向.Abstraction is a fundamental technique for solving the state-explosion problem in software model checking.In this paper,we survey a variety of abstract modeling formalisms that have been developed for this over the years.We first provide an overview of abstract software model checking based on the theoretical framework of abstract interpretation. We then discuss in detail several abstract modeling formalisms that are represented by 1）boolean Kripke structures,supporting traditional over-approximation or under-approximation;2）Kripke modal transition systems and mixed transition systems,respectively corresponding to 3-valued and 4-valued Kripke structures,supporting both over-approximation and under-approximation on a single model;and 3）models with hyper transitions,including generalized Kripke modal transition systems and hyper transition systems,allowing for more precise abstract model checking. We discuss the corresponding approximation relations and optimal abstract models,and highlight their shortcomings and the motivations for the development of new formalisms.We also introduce the completeness results of abstract modeling formalisms.Finally,we discuss the problems in theoretical and practical aspects of abstract models and point out future research directions.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]