模型检测是近二十年来最成功的形式化自动验证技术之一。其因自动化程度高,效率高等优点而被广泛应用于并发系统的分析与验证中。与定理证明等其他形式化验证方法相比,模型检测的主要优点在于:当断言被违反时,模型检测方法能够给出反例,以解释断言被违反的原因。然而,由于复杂系统的反例通常很长,导致非常难以理解,需要花费大量时间检查大量的变量和事件,才能够找到错误的根源。这些客观因素都影响了模型检测验证的效率。状态爆炸问题一直是模型检测的瓶颈问题。为了能够有效地应用模型检测方法,研究人员提出可以减少和压缩状态空间以缓解状态爆炸问题。因此,论文主要从模型检测的反例最小化分析、解决状态爆炸问题以及扩充Promela三个方面进行了研究,具体内容如下:1、介绍了Gastin.P最小反例算法思想,结合著名的Needham-Schroeder公钥身份认证协议对算法进行了非形式化分析,实例分析的结果表明了算法的有效性。在算法的基础上结合语法重定序策略提出了一种新的算法框架,解决了算法在搜索最小反例的过程中对状态的重复遍历的缺点。2、针对模型检测中存在的状态爆炸问题,从原子性、缩减随机数变量的取值范围、语法重定序以及偏序归约技术四个方面进行了研究。通过理论论述和实验验证相结合的方式说明了这些优化策略能有效地减少状态数。3、在Promela基本数据结构的基础上,扩充了栈和队列两种数据结构。主要是对顺序栈和循环队列进行了定义和实现。