ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2015, Vol. 52 ›› Issue (7): 1580-1603.doi: 10.7544/issn1000-1239.2015.20140413

• 综述 • 上一篇    下一篇

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

魏欧1,石玉峰1,徐丙凤1,2,黄志球1,陈哲1   

  1. 1(南京航空航天大学计算机科学与技术学院 南京 210016); 2(南京林业大学信息科学技术学院 南京 210037) (owei@nuaa.edu.cn)
  • 出版日期: 2015-07-01
  • 基金资助: 
    基金项目:国家自然科学基金项目(61170043,61100034,61272083);国家“九七三”重点基础研究发展计划基金项目(2014CB744904)

Abstract Modeling Formalisms in Software Model Checking

Wei Ou1, Shi Yufeng1, Xu Bingfeng1,2, Huang Zhiqiu1, Chen Zhe1   

  1. 1(College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016);2(College of Information Science and Technology, Nanjing Forestry University, Nanjing 210037)
  • Online: 2015-07-01

摘要: 抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为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),可提供更精确的抽象模型检测;重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果.最后,分析了目前关于抽象模型的理论和应用研究中存在的问题,给出进一步研究的方向.

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

Abstract: 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.

Key words: abstract models, over-approximation, under-approximation, model checking, multi-valued models

中图分类号: