| 软件模型检测中的抽象模型研究综述 |
| |
| 引用本文： | 魏欧,石玉峰,徐丙凤,黄志球,陈哲.软件模型检测中的抽象模型研究综述[J].计算机研究与发展,2015(7). |
| |
| 作者姓名： | 魏欧 石玉峰 徐丙凤 黄志球 陈哲 |
| |
| 作者单位： | 1. 南京航空航天大学计算机科学与技术学院 南京 210016
2. 南京航空航天大学计算机科学与技术学院 南京 210016; 南京林业大学信息科学技术学院 南京 210037 |
| |
| 基金项目： | 国家自然科学基金项目(61170043，61100034，61272083)；国家“九七三”重点基础研究发展计划基金项目 |
| |
| 摘 要： | 抽象是解决模型检测中状态爆炸问题的一个基本方法。对近年来软件模型检测研究中所提出的一系列抽象模型进行综述。首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分。然后根据模型的结构和功能特征，将抽象模型分为3类：1）传统的用于支持自上逼近或者自下逼近的布尔Kripke 结构；2）分别对应于3值和4值 Kripke 结构的 Kripke 模态迁移系统（Kripke modal transition systems ，KM TS）和混合迁移系统（mixed transition system ，MixTS），可同时支持自上逼近和自下逼近的抽象；3）具有超迁移关系的广义 Kripke 模态迁移系统（generalized Kripke modal transition system ，GKM TS）和超迁移系统（hyper transition system ，HTS），可提供更精确的抽象模型检测；重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果。最后，分析了目前关于抽象模型的理论和应用研究中存在的问题，给出进一步研究的方向。
|
| 关 键 词： | 抽象模型 自上逼近 自下逼近 模型检测 多值模型 |
Abstract Modeling Formalisms in Software Model Checking |
| |
| Wei Ou,Shi Yufeng,Xu Bingfeng,Huang Zhiqiu,Chen Zhe.Abstract Modeling Formalisms in Software Model Checking[J].Journal of Computer Research and Development,2015(7). |
| |
| Authors: | Wei Ou Shi Yufeng Xu Bingfeng Huang Zhiqiu Chen Zhe |
| |
| Abstract: | |
| |
| Keywords: | abstract models over-approximation under-approximation model checking multi-valued models |
| 本文献已被 万方数据 等数据库收录！ |
