摘要：模型检测(model checking)是一种能够自动验证有限状态并发系统的技术。该文从模型检测技术的背景入手,先阐述了模型检测技术基本原理及其相关过程。而后介绍了阻碍模型检测技术发展的状态爆炸问题,再者对Nu SMV、SPIN和UPPAAL等模型检测工具进行了介绍与比较。最后总结了模型检测技术在新的领域、工具研制、算法研究和与其他技术相结合等几个方面的研究进展,可为今后进一步对计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中提供借鉴。

关键词：模型检测技术 形式化验证 状态爆炸 状态约简 研究进展 

单位：西南交通大学