随着计算机技术的飞速发展，多处理器系统和多核芯片变得越来越常见。在设计各种复杂的计算机系统时，形式化验证技术在保证设计正确性和寻找系统漏洞方面也起着越来越重要的作用。人们提出了一系列形式化验证技术来帮助解决验证过程中遇到的困难问题。　　带参系统指拥有多个相同进程的系统，进程的数目指定了系统的参数。带参系统在实际应用中十分常见。从计算机中的多处理器架构到工业控制器，带参系统应用广泛。带参并发系统的验证问题一直是学术界和工业界研究的热点问题。带参验证的难点在于:对于给定参数的系统，可以证明其正确性，但是无法验证系统在任意参数下都是正确的。本文提出了一种基于不变量查找和定理证明的验证方法，设计实现了相应工具并对多种缓存协议进行建模验证，取得了一定的进展。　　本文的创新点主要体现在以下三个方面:　　1.设计实现了辅助不变量查找工具InvFinder并将该工具应用到缓存一致性协议的验证问题上。缓存一致性协议是一种典型的带参系统，InvFinder从缓存协议的小型参数实例出发，生成辅助不变量来帮助验证协议正确性。　　2.查找得到的辅助不变量、不变量和协议规则之间的对应关系可以用来构造形式化证明。使用定理证明工具Isabelle对自动生成的证明脚本进行验证，从而说明带参系统的正确性。　　3.将该方法应用到一系列常用的带参协议上，例如互斥协议、MESI协议、MOESI协议、GermanIsh协议、German协议，成功说明了这些带参协议的正确性。另外，通过查找得到的辅助不变量来分析协议的正确性，进一步帮助理解协议设计。