| 软件模型检测中的抽象模型研究综述 |
| |
| 引用本文： | 魏欧, 石玉峰, 徐丙凤, 黄志球, 陈哲. 软件模型检测中的抽象模型研究综述[J]. 计算机研究与发展, 2015, 52(7): 1580-1603. DOI: 10.7544/issn1000-1239.2015.20140413 |
| |
| 作者姓名： | 魏欧 石玉峰 徐丙凤 黄志球 陈哲 |
| |
| 作者单位： | 1.1(南京航空航天大学计算机科学与技术学院 南京 210016);2.2(南京林业大学信息科学技术学院 南京 210037) (owei@nuaa.edu.cn) |
| |
| 基金项目： | 国家自然科学基金项目(61170043,61100034,61272083);国家“九七三”重点基础研究发展计划基金项目 |
| |
| 摘 要： | 抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为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),可提供更精确的抽象模型检测;重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果.最后,分析了目前关于抽象模型的理论和应用研究中存在的问题,给出进一步研究的方向.
|
| 关 键 词： | 抽象模型 自上逼近 自下逼近 模型检测 多值模型 |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《计算机研究与发展》浏览原始摘要信息 |
|
点击此处可从《计算机研究与发展》下载免费的PDF全文 |
|
