模型检测技术研究综述

A Survey of Model Checking

从模型检测技术的研究背景入手,首先阐述了模型检测技术的基本原理和过程。然后介绍了制约模型检测技术发展的状态爆炸问题和一些状态约简技术,包括符号模型检测、on-the-fly技术、偏序归约和抽象技术,并对SPIN、NuSMV、UPPAAL和PAT等模型检测工具进行了介绍和比较。最后总结了模型检测技术在新的应用领域、工具研制、算法研究和与其它技术相结合等几个方面的研究进展。可为今后进一步对并发和实时系统进行建模、仿真和验证提供借鉴和参考。

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.