随着高性能计算机性能的不断提升、规模不断增大,Cache一致性协议变得异常复杂,协议的状态数随系统规模成指数级增长,导致状态空间爆炸。为了缓解状态空间爆炸问题对Cache一致性协议模型检验的影响,迫切需要研究模型检验优化技术。本文深入剖析了模型检验工具Murphi,介绍了Murphi的语法、模型检验的流程、执行模式和采用的优化技术。通过对简单协议进行验证,分析并总结出模型检验中状态数目与状态分量的值域之间的关系,并归纳出Murphi中状态空间分配规律,找出状态空间爆炸现象出现的原因。抽象是缓解状态空间爆炸问题的重要技术之一,它借助等价关系将原始模型映射到一个简化的抽象模型。抽象模型相对于原始模型大大化简,从而减少了模型检验时需要遍历的状态数目。本文提出了一种基于SMT求解器的谓词抽象技术。首先对高级描述语言Murphi进行BDD建模,将Murphi描述转换成相应的BDD公式；然后结合给定的谓词,将抽象问题转换成可满足性模型理论问题,并利用最新的SMT求解器进行求解；最后利用模型检验工具对抽象模型进行验证。实验表明,基于SMT求解器的谓词抽象能够在保证验证结果正确的同时显著减少对状态空间的需求。文章对谓词抽象的关键算法进行了分析,采用非递归方式实现下一抽象状态的计算,提高了谓词抽象的效率。详细分析了经典的Cache一致性协议,给出了共享读、独占写和数据写回三种处理流程的消息传递规则。对谓词抽象前后的Cache协议进行模型检验,比较了两种方法在验证时间和空间上的差别。实验结果表明基于谓词抽象的模型检验能够减少验证所需的状态空间,满足更大规模系统的验证需求。