| 模型检测技术研究综述 |
| |
| 引用本文： | 化希耀,苏博妮,陈立平,高贤强.模型检测技术研究综述[J].塔里木农垦大学学报,2013(4):119-124. |
| |
| 作者姓名： | 化希耀 苏博妮 陈立平 高贤强 |
| |
| 作者单位： | [1]塔里木大学信息工程学院,新疆阿拉尔843300 [2]上海海事大学信息工程学院,上海201306 |
| |
| 基金项目： | 国家自然科学基金（61162018）;塔里木大学校长基金项目（TDZKSS201320）. |
| |
| 摘 要： | 从模型检测技术的研究背景人手，首先阐述了模型检测技术的基本原理和过程。然后介绍了制约模型检测技术发展的状态爆炸问题和一些状态约简技术，包括符号模型检测、Oil—the—fly技术、偏序归约和抽象技术，并对SPIN、NuSMV、UP-PAAL和PAT等模型检测工具进行了介绍和比较。最后总结了模型检测技术在新的应用领域、工具研制、算法研究和与其它技术相结合等几个方面的研究进展。可为今后进一步对并发和实时系统进行建模、仿真和验证提供借鉴和参考。
|
| 关 键 词： | 模型检测 形式化验证 状态爆炸 状态约简 研究进展 |
A Survey of Model Checking |
| |
| ,Hua XiyaoI Su Boni,Chen LipingI Gao Xianqiang.A Survey of Model Checking[J].Journal of Tarim University of Agricultural Reclamation,2013(4):119-124. |
| |
| Authors: | ,Hua XiyaoI Su Boni,Chen LipingI Gao Xianqiang |
| |
| Institution: | (2 Hua XiyaoI Su Boni2 Chen LipingI Gao Xianqiang1. (1 College of Information Engineering, Tarim University, Alar, Xinjiang 843300) College of Information Engineering, Shanghai Maritime University, Shanghai 201306 ) |
| |
| Abstract: | Basic principles and processes of model checking are given, and the notorious state explosion problem and some state - of - the - art reduction techniques are introduced, including symbolic model checking, partial order reduction, on - the - fly and abstrac- tion techniques. Further more, a comparison on some distinguished model checking tools, including SPIN, NuSMV, UPPAAL and PAT is given. Finally, a summarization about the progress of model checking is presented and provides beneficial references to further studying on model checking. |
| |
| Keywords: | model checking formal verification state explosion state reduction research progress |
| 本文献已被 维普 等数据库收录！ |
|
