随着计算机技术、网络技术以及电子信息技术在各行各业的日益发展,多处理器体系以及多核架构在计算机系统结构中应用得越来越频繁,其正确性、可靠性等问题也越来越突出。带参协议在计算机系统多处理器体系的核心结构中广泛存在,面对日趋复杂的设计,带参协议正确性的验证越来越成为设计流程中的关键,细微的错误可能引发严重的后果。因此,带参协议设计正确性的验证问题成为了学术界和工业界研究的热点和重点。形式化验证方法通过符号描述带参协议的系统行为及其性质,基于各种数学逻辑推理算法进行验证,验证覆盖率高,且具有完备性,目前已经成为带参协议验证的重要方法。在带参协议形式化验证领域,虽然己经存在多种形式化验证方法,但是每种方法都存在一定的缺点,例如定理证明技术的自动化程度不高,需要人为主动干预,模型检测技术在带参协议规模较大的情况下会出现状态空间爆炸的问题,这些都成为了限制带参协议形式化验证有效性的重要因素。本论文对现有的带参协议的形式化验证方法进行了分类整理和深入分析,主要从提高定理证明技术的自动化程度和缓解模型检测技术状态空间的爆炸现象两个角度入手,提出了两种验证方法,并且在MESI、MutualEx、GERMAN、FLASH等典型的带参协议上验证了它们的有效性,主要的研究成果如下:(1)提出了一种基于归纳不变式和流分析结合的验证方法。该方法分析了带参协议的不变式和迁移规则实例之间存在的因果关系,通过归纳不变查找算法自动查找带参协议的归纳不变式,为使用定理证明工具构造定理证明脚本提供了便利。除此之外,引入了流分析的概念,在验证前期对带参协议的内容进行了流分析,将归纳不变式和流分析结合起来进一步对带参协议进行了验证。本文给出了该方法的整体框架和具体实现,并在多个典型带参协议中验证了该方法的有效性。(2)提出了一种基于CVC4的谓词抽象的验证方法。该方法将谓词抽象的思想应用到Murphi模型检测技术中,借助CVC4求解器求出带参协议原有状态对应的抽象状态,把系统性质的验证从原始状态转移到抽象状态,在一定程度上解决了模型检测技术中随着带参协议规模增大而出现的状态空间爆炸问题。实验结果表明基于CVC4的谓词抽象的验证方法能显著缩减带参协议的状态空间。