协议广义上指网络协议,协议的功能是用于描述模块间的通讯规则,本文中,协议狭义地指由卫式命令语言(Guarded Command Language)描述的协议程序。带参协议是参数化后的协议,是协议的推广形式。带参协议应用广泛,如互斥协议、缓存一致性协议、网络安全通信协议等都属于带参协议。带参协议验证是对带参协议逻辑正确性进行校验的过程,其目的是为了保障带参协议满足设计要求。协议的传统形式化验证方法,是通过枚举协议的所有可达状态,来依次验证协议的设计要求是否在每个状态下均成立,然而,这种验证方式不适合带参协议验证。其主要原因是:一是带参协议拥有无数个实例,而每个实例都等价于一个协议,直接验证所有实例非常困难;二是带参协议实例的状态数量随参数增加成指数级增长,造成状态爆炸问题,导致大参数带参协议实例难以验证。为了解决协议验证方法难以应用于带参协议验证的问题,带参协议验证专家提出了各自的解决方法,如抽象方法、截止方法和归纳证明方法等等。其中,归纳证明方法被认为是最可行的解决方案之一。使用归纳证明方法验证带参协议需要寻找辅助不变式,传统的辅助不变式寻找方式为人工推导,这种方法只适用于小型带参协议的验证,对于大型带参协议,人工推导方法不仅实现困难而且容易出错,这使得归纳证明方法难以推广。为了解决归纳证明方法中辅助不变式的寻找问题,本文提出了基于决策树的不变式判断方法,并结合现有的带参协议归纳证明技术,提出了基于决策树的带参协议自动化验证方法。基于决策树的带参协议自动化验证方法是首个将决策树方法应用于带参协议验证的方法。该方法可以高效地寻找辅助不变式并完成带参协议的归纳证明。基于决策树的带参协议自动化验证方法主要有以下创新点:(1)提出了使用带参协议实例的对称削减可达状态集合作为决策树训练数据的方法。使用这种训练数据不仅使决策树能够准确判断候选不变式,而且减少了决策树的生成和判断候选不变式所需要的内存与时间。(2)提出了针对带参协议实例的决策树算法。这种算法以ID3算法为基础,通过修改决策树叶子节点的生成条件与生成方法,使决策树包含了更多有关带参协议实例的信息,从而保证决策树能够准确无误地判断候选不变式。(3)提出了使用决策树路径判断候选不变式的方法。这种方法的原理是利用决策树路径与候选不变式的关系,使用可达状态类别判断候选不变式是否为带参协议实例的不变式。基于决策树的带参协议自动化验证方法针对的带参协议类型是缓存一致性协议。试验证明,基于决策树的带参协议自动化验证方法能够应用于包含Flash协议的多种典型带参协议,并且和ParaVerifier方法相比,在验证大型带参协议时,时间消耗与内存占用方面均有明显优势。