第5章-协议验证技术ppt课件

1、南京邮电大学南京邮电大学第第 5 章章 协议验证技术协议验证技术第第5章章 协议验证技术协议验证技术 内容提要内容提要概述概述1协议性质协议性质2可达性分析可达性分析3不变性分析不变性分析4第第5章章 协议验证技术协议验证技术 协议验证协议验证vHolzman：每一个新设计的协议在被完全证明：每一个新设计的协议在被完全证明没有错误之前，都应认为不是完全正确的。没有错误之前，都应认为不是完全正确的。v协议验证技术和形式描述技术是同步发展的，协议验证技术和形式描述技术是同步发展的，它也是协议工程技术中研究最早、最深入的课它也是协议工程技术中研究最早、最深入的课题，使用的技术方法多种多样。题，使用的

2、技术方法多种多样。 第第5章章 协议验证技术协议验证技术 验证的含义验证的含义v“验证的含义：验证的含义： v验证协议的设计。验证协议的设计。v通过分析每一层的所有协议实体间的所有可能的通过分析每一层的所有协议实体间的所有可能的交互、协议的抽象规范中所确定的功能以及通过交互、协议的抽象规范中所确定的功能以及通过低层提供的服务所实现的对等层间的通信来确定低层提供的服务所实现的对等层间的通信来确定上述操作是否满足协议的服务规范。上述操作是否满足协议的服务规范。v在设计阶段进行验证，可以及早发现协议错误，在设计阶段进行验证，可以及早发现协议错误，大大降低协议开发成本。大大降低协议开发成本。 v验证协

3、议的实现。验证协议的实现。v检查每一个协议实体的实现是否满足它的抽象协检查每一个协议实体的实现是否满足它的抽象协议规范。大多数情况下，协议实现的验证是通过议规范。大多数情况下，协议实现的验证是通过不同的测试工具来实现的。不同的测试工具来实现的。v有时也将其称为协议实现评估或协议的一致性测有时也将其称为协议实现评估或协议的一致性测试试 一般情况下，协议验证指的是第一般情况下，协议验证指的是第(1)(1)类验类验证，这也是本课程的观点。具体来说，协证，这也是本课程的观点。具体来说，协议验证是指根据协议规范来检查协议实体议验证是指根据协议规范来检查协议实体间的交互是否满足一定特性间的交互是否满足一定

4、特性(properties)(properties)或条件或条件(conditions)(conditions)的过程，例如，检查的过程，例如，检查是否有死锁存在。通过协议验证，可以获是否有死锁存在。通过协议验证，可以获知协议设计是否满足正确性、完整性和一知协议设计是否满足正确性、完整性和一致性等要求。致性等要求。 第第5章章 协议验证技术协议验证技术 Verification and Validationv 在英文文献中，在英文文献中，“验证一词有两种不同的表示：验证一词有两种不同的表示：validationvalidation和和verificationverification。它们的含义

5、也比较混乱。它们的含义也比较混乱。 v 文献文献Rud98Rud98以为以为: :v validationvalidation主要是指检查协议逻辑上的一致性，以查主要是指检查协议逻辑上的一致性，以查实协议设计中是否存在某些错误，这些错误是所有协实协议设计中是否存在某些错误，这些错误是所有协议中都可能存在的共性错误，与具体的协议功能无关，议中都可能存在的共性错误，与具体的协议功能无关，例如，验证有无死锁。例如，验证有无死锁。v 而而verificationverification则是指检查协议是否能成功地提供指则是指检查协议是否能成功地提供指定的协议功能。定的协议功能。 v 文献文献Lai98L

6、ai98以为以为: :v verificationverification主要是指检查一个系统是否满足它的规主要是指检查一个系统是否满足它的规格说明，格说明，v 而而validationvalidation的含义则不仅包括的含义则不仅包括verificationverification，还可，还可能包括对最终的系统实现进行测试，系统模拟，性能能包括对最终的系统实现进行测试，系统模拟，性能分析预测等。分析预测等。 第第5章章 协议验证技术协议验证技术 Verification and ValidationvBohem：vVerification: to establish the truth o

7、f correspondence between a software product and its specification (“truth”) or are we building the product right?vValidation: to establish the fitness or worth of a software product for its operational mission (“to be worth”)v or are we building the right product?v谢谢94版网络书中介绍：版网络书中介绍：vVerification:

8、在功能方面进行验证在功能方面进行验证vValidation: 在语法方面进行证实在语法方面进行证实v在实践当中，在实践当中，validation和和verification所采用的技所采用的技术并没有明显的界限。也正因为如此，很多文献术并没有明显的界限。也正因为如此，很多文献并没有严格区分并没有严格区分validation和和verification，而是混，而是混用这两个单词。用这两个单词。第第5章章 协议验证技术协议验证技术 Verification and Validation第第5章章 协议验证技术协议验证技术 形式化验证形式化验证v非形式化验证则主要通过传统的遍历非形式化验证则主要通

9、过传统的遍历(walkthrough)(walkthrough)和代码检查和代码检查(inspection)(inspection)来实来实现。现。v协议验证通常与形式描述技术有关。形式化验协议验证通常与形式描述技术有关。形式化验证主要将形式描述技术和推理技术相结合，是证主要将形式描述技术和推理技术相结合，是形式化描述技术的一个重要方面，其优点是：形式化描述技术的一个重要方面，其优点是：v一方面可以获得无二义性的协议规范，一方面可以获得无二义性的协议规范，v另一方面可以通过计算机辅助工具来帮助实施另一方面可以通过计算机辅助工具来帮助实施自动或半自动验证。自动或半自动验证。 v协议设计者必须在早

10、期的协议设计阶段采用一协议设计者必须在早期的协议设计阶段采用一些技术或工具来发现设计中存在的错误，这也些技术或工具来发现设计中存在的错误，这也是协议验证的最重要的目的。是协议验证的最重要的目的。 第第5章章 协议验证技术协议验证技术 形式化协议验证形式化协议验证v主要两类方法：主要两类方法：v模型检测模型检测Model Checking）：基于状态搜索）：基于状态搜索State Exploration）v演绎验证演绎验证Deductive Verification）：基于定理证）：基于定理证明明Theorem Proving）第第5章章 协议验证技术协议验证技术 模型检测方法模型检测方法v步骤

11、：步骤：v建模建模Modeling）v描画描画Specification）v验证验证Verification）v问题：状态空间爆炸问题：状态空间爆炸v协议运行的无穷状态空间的不可搜索性协议运行的无穷状态空间的不可搜索性 v协议运行过程中的无穷消息空间的不可搜索性协议运行过程中的无穷消息空间的不可搜索性 第第5章章 协议验证技术协议验证技术 定理证明方法定理证明方法v步骤：步骤：v将实现方案和功能描述都转换为一种形式逻辑，将实现方案和功能描述都转换为一种形式逻辑，如命题逻辑、一阶逻辑如命题逻辑、一阶逻辑First Order Logic, FOL）、高阶逻辑）、高阶逻辑Higher Order

12、Logic, HOL等等 v建立公理系统，作为验证的依据，并将协议性质建立公理系统，作为验证的依据，并将协议性质构造成一组代定数定理构造成一组代定数定理 v根据公理系统，使用定理证明器，通过逻辑推理、根据公理系统，使用定理证明器，通过逻辑推理、逻辑规约等手段，构造证明过程，证明实现方案逻辑规约等手段，构造证明过程，证明实现方案和功能描述等价和功能描述等价 v问题：入门难，前两步难问题：入门难，前两步难第第5章章 协议验证技术协议验证技术 内容提要内容提要概述概述1协议性质协议性质2可达性分析可达性分析3不变性分析不变性分析4第第5章章 协议验证技术协议验证技术 协议性质协议性质v 协议验证的最

13、主要内容是检查协议是否满足规定协议验证的最主要内容是检查协议是否满足规定的协议性质。一般情况下，将协议性质分为两类：的协议性质。一般情况下，将协议性质分为两类：v一般性质一般性质(general properties)。指所有协议所具有。指所有协议所具有的一些公共特性。不同文献对这类性质的个数和的一些公共特性。不同文献对这类性质的个数和描述也不尽相同。描述也不尽相同。v特殊性质特殊性质(specific properties)。是指与具体协议内。是指与具体协议内容有关的性质。对这些性质的定义构成了服务规容有关的性质。对这些性质的定义构成了服务规范的主体内容。范的主体内容。 v也有文献将协议性质

14、分为安全性也有文献将协议性质分为安全性(safety)和活跃性和活跃性(liveness)。第第5章章 协议验证技术协议验证技术 一般性质一般性质v 可达性可达性(Reachability)(Reachability)。验证协议的各种可能状态之间的可。验证协议的各种可能状态之间的可达关系。如果协议的某个状态从初态不可达，则表明协议有达关系。如果协议的某个状态从初态不可达，则表明协议有错误。如果从状态错误。如果从状态A A到状态到状态B B的变迁不可能发生的变迁不可能发生( (直接或间接直接或间接) )，则从状态则从状态A A到状态到状态B B是不可达的。是不可达的。 v 没有死锁没有死锁(De

15、adlock freeness)(Deadlock freeness)。最典型的死锁是协议中各。最典型的死锁是协议中各实体都处于这样的一种等待状态，即只有在实体都处于这样的一种等待状态，即只有在“某一事件发某一事件发生后才能做进一步的动作，但在该状态下，这个生后才能做进一步的动作，但在该状态下，这个“某一事件某一事件却不可能发生。死锁发生时，协议所处的状态称为死锁状却不可能发生。死锁发生时，协议所处的状态称为死锁状态。态。 v 没有活锁没有活锁(Livelock freeness) (Livelock freeness) 。活锁是指协议处于无限。活锁是指协议处于无限的死循环中，而没有别的事件可

16、使协议从这一循环中解脱出的死循环中，而没有别的事件可使协议从这一循环中解脱出来。例如，协议无限制地执行超时重发操作，但总是收不到来。例如，协议无限制地执行超时重发操作，但总是收不到对方的确认信息。状态还是在变化的，不过不能脱离这种死对方的确认信息。状态还是在变化的，不过不能脱离这种死循环状态而已。循环状态而已。 第第5章章 协议验证技术协议验证技术 一般性质一般性质Cont.）v 弱活锁弱活锁(Weak livelock)(Weak livelock)。是指协议处于死循环中，只有。是指协议处于死循环中，只有当协议交换命令的相对速度达到某一状态时，协议才退出当协议交换命令的相对速度达到某一状态时

17、，协议才退出死循环。死循环。v 时间相关的活锁时间相关的活锁(Time-dependent livelock)(Time-dependent livelock)。也称为临。也称为临时阻塞时阻塞(Tempo-blocking)(Tempo-blocking)。它是指协议处于死循环中，但。它是指协议处于死循环中，但是当通信双方交换报文的相对速度到达某一状态时，协议是当通信双方交换报文的相对速度到达某一状态时，协议可以从死循环中出来。可以从死循环中出来。v 有界性有界性(Boundedness)(Boundedness)。检验协议的某些成分或参数的容。检验协议的某些成分或参数的容量量( (例如：通道

18、容量、窗口大小例如：通道容量、窗口大小) )是否有界。有界性是针对是否有界。有界性是针对协议元素性质和通道性质而言。协议元素性质和通道性质而言。v 可恢复性或自同步性可恢复性或自同步性Recovery from failuresRecovery from failures）。这是）。这是当出现差错后，协议能否在有限的步骤内返回到正常状态当出现差错后，协议能否在有限的步骤内返回到正常状态( (包括初始态包括初始态) )执行。执行。 第第5章章 协议验证技术协议验证技术 一般性质一般性质Cont.）v 无状态二义性无状态二义性(State ambiguities freeness)(State a

19、mbiguities freeness)。一个进程。一个进程在某一时刻只允许具有一个稳定状态。所谓稳定状态是指在某一时刻只允许具有一个稳定状态。所谓稳定状态是指当通信双方的通道为空时的进程状态。若在某一时刻进程当通信双方的通道为空时的进程状态。若在某一时刻进程可以有多个稳定状态，则称该进程的状态为二义状态。可以有多个稳定状态，则称该进程的状态为二义状态。v 互斥性互斥性(Mutual exclusion)(Mutual exclusion)。互斥性是指有些协议动作不。互斥性是指有些协议动作不能同时被多个用户执行。例如，多个用户不能同时请求同能同时被多个用户执行。例如，多个用户不能同时请求同一资

20、源。一资源。 v 终止或进展终止或进展(Termination or Progress)(Termination or Progress)。是指协议提供。是指协议提供的服务必须在有限时间内完成。的服务必须在有限时间内完成。v 终止是针对终止协议终止是针对终止协议(terminating protocols)(terminating protocols)而言，意而言，意思是指协议总是能到达期望的结束状态。思是指协议总是能到达期望的结束状态。v 而进展则是针对循环协议而进展则是针对循环协议(cyclic protocols)(cyclic protocols)而言，意思而言，意思是指协议总是能到达

21、它的初始状态。是指协议总是能到达它的初始状态。 第第5章章 协议验证技术协议验证技术 一般性质一般性质Cont.）v无冗余描述无冗余描述(Absence of Overspecification)(Absence of Overspecification)。协议规范中没有无用的、冗余描述，例如，没协议规范中没有无用的、冗余描述，例如，没有未经实践的报文接收有未经实践的报文接收(absence of (absence of unexercised message receptions)unexercised message receptions)。 v公平性公平性(Fairness)(Fairn

22、ess)。是指每一个协议实体均应。是指每一个协议实体均应平等地得到运行的机会，无论其它的协议实体平等地得到运行的机会，无论其它的协议实体想做什么。想做什么。 第第5章章 协议验证技术协议验证技术 特殊性质特殊性质v完整性完整性(Completeness)(Completeness)。是指协议设计考虑了所。是指协议设计考虑了所有可能发生的事件、选项以及服务。检验协议是有可能发生的事件、选项以及服务。检验协议是否能处理所有可能的输入，即是否缺少应用的处否能处理所有可能的输入，即是否缺少应用的处理，或有无非期待的接收或输入理，或有无非期待的接收或输入( (即错收即错收) )。也有。也有的文献将完整性

23、称为完全正确性的文献将完整性称为完全正确性(complete (complete correctness)correctness)。v一致性一致性(consistency)(consistency)。是指协议服务行为。是指协议服务行为( (或性或性质质) )和协议行为和协议行为( (或性质或性质) )一致，即协议应该提供用一致，即协议应该提供用户要求的服务，而无需提供用户没有要求的服务。户要求的服务，而无需提供用户没有要求的服务。也有文献将一致性称为部分正确性也有文献将一致性称为部分正确性(partial (partial correctness)correctness)、等价性、等价性(eq

24、uivelence)(equivelence)等。等。 第第5章章 协议验证技术协议验证技术 一般性质一般性质 vs. 特殊性质特殊性质v协议验证着重在于一般性质，而协议测试则着重协议验证着重在于一般性质，而协议测试则着重于特殊性质。于特殊性质。 第第5章章 协议验证技术协议验证技术 安全性安全性(safety) vs. 活动性活动性(liveness)v 安全性安全性v 是指协议的所有动作均需与它的服务规范保持一致，即没是指协议的所有动作均需与它的服务规范保持一致，即没有不期望的情况出现。有不期望的情况出现。v 不期望的情况包括：不可接收的事件、不可进一步向前的不期望的情况包括：不可接收的事

25、件、不可进一步向前的状态、错误的动作、错误的条件、变量值越界等。状态、错误的动作、错误的条件、变量值越界等。v 例如，如果传输协议传送报文，则它必须将这些报文传送例如，如果传输协议传送报文，则它必须将这些报文传送到正确的目的地，按正确的顺序，并且无差错地交给目的到正确的目的地，按正确的顺序，并且无差错地交给目的主机。主机。v 安全性保证协议不出现错误。安全性保证协议不出现错误。v 活动性活动性v 是指在有穷时间内，完成规范所规定的动作是指在有穷时间内，完成规范所规定的动作(或所有的服或所有的服务必须在有限时间内完成务必须在有限时间内完成)。v 在进行逻辑验证时，确保一个有限的时延就足够了。但是

26、，在进行逻辑验证时，确保一个有限的时延就足够了。但是，在验证协议的效率和响应能力时，则必须定量地确定期望在验证协议的效率和响应能力时，则必须定量地确定期望的时延、吞吐率以及其它的一些指标。的时延、吞吐率以及其它的一些指标。 第第5章章 协议验证技术协议验证技术 安全性安全性(safety) vs. 活动性活动性(liveness)v 活动性活动性(Cont.)v 协议的活动性体现在终止性协议的活动性体现在终止性(termination)和进展性和进展性(progress)两个方面。两个方面。 v 终止性是指协议从任何一个状态开始运行，经过有限时间终止性是指协议从任何一个状态开始运行，经过有限时

27、间总能正确地达到终止状态；总能正确地达到终止状态；v 进展性是指协议从初始状态运行，经过有限时间总能到达进展性是指协议从初始状态运行，经过有限时间总能到达指定状态。指定状态。 v 在某些情况下，终止状态和初始状态是同一的。这样，协在某些情况下，终止状态和初始状态是同一的。这样，协议从初始状态出发总能正确地回到初始状态，并可反复运议从初始状态出发总能正确地回到初始状态，并可反复运行。行。 第第5章章 协议验证技术协议验证技术 内容提要内容提要概述概述1协议性质协议性质2可达性分析可达性分析3不变性分析不变性分析4第第5章章 协议验证技术协议验证技术 协议验证方法协议验证方法v 验证方法主要有两类

28、：验证方法主要有两类：v 模型检查模型检查(Model Checking)(Model Checking)。最常见方法：。最常见方法：v 可达性分析可达性分析(RA: Reachability analysis) (RA: Reachability analysis) ，它包括，它包括状态穷举，状态随机枚举，状态概率枚举等方法状态穷举，状态随机枚举，状态概率枚举等方法 v 不变性分析不变性分析(invariance analysis)(invariance analysis)v 等价性分析等价性分析(equivalence analysis)(equivalence analysis)v 重要

29、问题：状态空间爆炸重要问题：状态空间爆炸 v 证明证明(Proving)(Proving)v 试图用推理演算方法严密地证明协议的各种性质试图用推理演算方法严密地证明协议的各种性质v 其他方法：其他方法：v 模拟模拟SimulationSimulation）v 通过一些模拟试验来测试协议的各种性质通过一些模拟试验来测试协议的各种性质第第5章章 协议验证技术协议验证技术 可达性分析可达性分析一、概一、概 述述第第5章章 协议验证技术协议验证技术 可达性分析可达性分析v可达性分析是最常用的协议验证方法。它试图可达性分析是最常用的协议验证方法。它试图产生和检查协议所有或部分可达状态。产生和检查协议所有

30、或部分可达状态。v“可达状态是指协议从初始状态开始经历有可达状态是指协议从初始状态开始经历有限次转换之后可达到的状态。限次转换之后可达到的状态。v所有可达状态构成可达图所有可达状态构成可达图(RG: Reachability (RG: Reachability Graph)Graph)。第第5章章 协议验证技术协议验证技术 可达性分析可达性分析Cont.）v可达性分析的原理是可达性分析的原理是: :v采用穷举法检查同一层内两个或多个协议实体间采用穷举法检查同一层内两个或多个协议实体间所有可能的交互所产生的状态。所有可能的交互所产生的状态。v将协作的协议实体的状态以及连接这些协议实体将协作的协议

31、实体的状态以及连接这些协议实体的低层称为系统的全局状态或混合状态的低层称为系统的全局状态或混合状态(composite or global state)(composite or global state)。v从一个给定的初始状态开始，所有可能的变迁从一个给定的初始状态开始，所有可能的变迁( (用用户命令、超时、报文到达等户命令、超时、报文到达等) )产生许多新的全局状产生许多新的全局状态。态。v对每一个新产生的状态重复执行上述过程直到没对每一个新产生的状态重复执行上述过程直到没有新的状态产生有新的状态产生( (某些变迁将导致系统返回到已产某些变迁将导致系统返回到已产生的状态生的状态) )。

32、v对于一个给定的初始状态和一组关于低层协议的对于一个给定的初始状态和一组关于低层协议的假定假定( (提供的服务的类型提供的服务的类型) )，这种分析能够确定协，这种分析能够确定协议可能产生的所有结果。议可能产生的所有结果。 第第5章章 协议验证技术协议验证技术 可达性分析续）可达性分析续）v 可达性分析最适合于用状态变迁模型描述的协议模型。可达性分析最适合于用状态变迁模型描述的协议模型。v 对于状态变迁模型的全局状态空间的产生也比较容易自动对于状态变迁模型的全局状态空间的产生也比较容易自动化，目前已有很多作此用途的工具。化，目前已有很多作此用途的工具。v 对于程序语言描述的协议模型也可以使用可

33、达性分析方法。对于程序语言描述的协议模型也可以使用可达性分析方法。v 具体做法是：在程序中设置许多断点具体做法是：在程序中设置许多断点(break points)(break points)，这，这些断点有效地定义了系统的控制状态。些断点有效地定义了系统的控制状态。v 可达性分析方法特别适用于验证上一节提到的协议的一般可达性分析方法特别适用于验证上一节提到的协议的一般性质，因为这些性质是可达图结构的一种直接结果。性质，因为这些性质是可达图结构的一种直接结果。v 没有出口的全局状态要么是死锁，要么是期望的结束状态。没有出口的全局状态要么是死锁，要么是期望的结束状态。v 同样，收到一个没有定义如何

34、处理的报文或超过了传输媒同样，收到一个没有定义如何处理的报文或超过了传输媒体的带宽等情况很容易被发现。体的带宽等情况很容易被发现。 第第5章章 协议验证技术协议验证技术 可达性分析可达性分析Cont.）v可达性分析涉及三个重要技术：可达性分析涉及三个重要技术： v怎样找出所有可达状态，构成可达图。怎样找出所有可达状态，构成可达图。 v怎样检测死锁、活锁等协议错误。怎样检测死锁、活锁等协议错误。 v怎样解决状态空间爆炸问题。怎样解决状态空间爆炸问题。 第第5章章 协议验证技术协议验证技术 可达性分析可达性分析二、可达性分析算法二、可达性分析算法第第5章章 协议验证技术协议验证技术 可达性分析算法

35、可达性分析算法v文献文献Holz93Holz93给出了三个主要的可达性分析算法：给出了三个主要的可达性分析算法：v穷尽性可达性分析算法穷尽性可达性分析算法(exhaustive or full (exhaustive or full search)search)，v受控部分搜索算法受控部分搜索算法(controlled partial (controlled partial search)search)，v随机模拟算法随机模拟算法(random simulation)(random simulation)。 第第5章章 协议验证技术协议验证技术 算法一：穷尽性可达性分析算法算法一：穷尽性可达性

36、分析算法 start() W = 初始状态初始状态; /* 工作集：分析的状态工作集：分析的状态 */ A = ; /* 已分析过的状态已分析过的状态 */ analyze(); analyze() /* 全局搜索全局搜索 */ if (W为空为空) return; q = 取自取自W的元素；的元素； 将将q加入到加入到A中中 if (q是错误状态是错误状态) report_error(); /* 报告错误报告错误 */ else for (q的每一个后继状态的每一个后继状态s) if (s不在不在A或或W中中) 把把s加入到加入到W中；中；analyze(); 从从W中删除中删除q； 工作集

37、工作集W W控制系统状态空间树的搜索控制系统状态空间树的搜索顺序。如果工作集顺序。如果工作集W W中的状态以先进中的状态以先进先出先出FIFOFIFO的顺序取出，那么算法的顺序取出，那么算法执行的是状态空间树的先广搜索执行的是状态空间树的先广搜索breadth-firstbreadth-first）；如果以先进后）；如果以先进后出出FILOFILO的顺序取出，则是状态空的顺序取出，则是状态空间树的先深搜索间树的先深搜索(deapth-first)(deapth-first)。先深搜索方法占用存贮空间小，这是先深搜索方法占用存贮空间小，这是其最大优点之一。其最大优点之一。 假定每个状态有两个后假

38、定每个状态有两个后继状态，算法执行继状态，算法执行m m步之步之后，对于先深搜索方法，后，对于先深搜索方法，W W的长度为的长度为m m，而对于先，而对于先广搜索方法，广搜索方法，W W的长度为的长度为2m2m。 第第5章章 协议验证技术协议验证技术 算法一：穷尽性可达性分析算法算法一：穷尽性可达性分析算法 start() W = 初始状态初始状态; /* 工作集：分析的状态工作集：分析的状态 */ A = ; /* 已分析过的状态已分析过的状态 */ analyze(); analyze() /* 全局搜索全局搜索 */ if (W为空为空) return; q = 取自取自W的元素；的元素

39、； 将将q加入到加入到A中中 if (q是错误状态是错误状态) report_error(); /* 报告错误报告错误 */ else for (q的每一个后继状态的每一个后继状态s) if (s不在不在A或或W中中) 把把s加入到加入到W中；中；analyze(); 从从W中删除中删除q； 第第5章章 协议验证技术协议验证技术 算法一：穷尽性可达性分析算法算法一：穷尽性可达性分析算法v上述算法假定用来进行验证的计算机的存贮空间上述算法假定用来进行验证的计算机的存贮空间足够大，且计算速率足够高。这往往是不现实的。足够大，且计算速率足够高。这往往是不现实的。v因此，大多数情况下，只有将协议验证模

40、型化简因此，大多数情况下，只有将协议验证模型化简到给定机器能够分析的程度时基于这种算法的验到给定机器能够分析的程度时基于这种算法的验证才可行。证才可行。v一般采用结构化或分层的方法来降低模型的复杂一般采用结构化或分层的方法来降低模型的复杂性。性。v但在某些情况下，由于被分析的问题的固有复杂但在某些情况下，由于被分析的问题的固有复杂性，只能将模型化简到一定程度，因为如果再进性，只能将模型化简到一定程度，因为如果再进一步化简则可能丢失其基本的、重要的性质。一步化简则可能丢失其基本的、重要的性质。v由此产生了另外一种搜索算法，即受控部分搜索由此产生了另外一种搜索算法，即受控部分搜索算法。算法。 第第

41、5章章 协议验证技术协议验证技术 算法二：受控部分搜索算法算法二：受控部分搜索算法/* start()与算法与算法5.1中的相同中的相同 */analyze() /* 部分搜索部分搜索 */ if (W为空为空) return; q = 取自取自W的元素；的元素； 将将q加入到加入到A中中 if (q是错误状态是错误状态) report_error(); /* 报告错误报告错误 */ else for (q的某些后继状态的某些后继状态s) if (s不在不在A或或W中中) 把把s加入到加入到W中；中；analyze(); 从从W中删除中删除q； 选择状态的规则有很多，例如，选择状态的规则有很多

42、，例如，限制深度法限制深度法(Depth-bounds)(Depth-bounds)，散开搜索散开搜索(Scatter Search)(Scatter Search)，定向搜索法定向搜索法(Guided Search)(Guided Search)，概率法概率法(Probabilistic (Probabilistic Search)Search)，启发式，启发式Yu91Yu91，随机，随机选择法选择法(Random (Random Selections)West87Selections)West87，状态矢，状态矢量法量法Holz91Holz91等等 算法不考虑检查协议所有可算法不考虑检查协

43、议所有可能的状态，而是预先确定满能的状态，而是预先确定满足某些要求足某些要求( (如，死锁如，死锁) )的潜的潜在的全局状态，然后检查这在的全局状态，然后检查这些状态是否可达。些状态是否可达。 第第5章章 协议验证技术协议验证技术 算法二：受控部分搜索算法算法二：受控部分搜索算法v 限制深度法。限制深度法。v 原理是限制被分析的执行序列的长度，从而只需分析协议原理是限制被分析的执行序列的长度，从而只需分析协议行为的一个子集。实质上，限制了完全搜索算法中的工作行为的一个子集。实质上，限制了完全搜索算法中的工作集集W的大小。限制深度法是一种相当标准和简单的部分搜的大小。限制深度法是一种相当标准和简

44、单的部分搜索技术。索技术。 v 散开搜索法。散开搜索法。v 原理是尽可能选择有可能导致死锁的执行序列来进行检查，原理是尽可能选择有可能导致死锁的执行序列来进行检查，从而增加尽快发现错误的概率。例如，死锁的一个前提条从而增加尽快发现错误的概率。例如，死锁的一个前提条件是没有待处理的报文件是没有待处理的报文(通道为空通道为空)，因此，这种算法更可，因此，这种算法更可能去检查报文接收操作而不是发送操作。能去检查报文接收操作而不是发送操作。 v 定向搜索法。定向搜索法。v 在定向搜索法中，为每一个后继状态计算它的代价函数值在定向搜索法中，为每一个后继状态计算它的代价函数值(cost function)

45、。然后，根据这个计算结果作为是否执行它。然后，根据这个计算结果作为是否执行它的依据。代价函数在搜索过程中可以动态地改变。的依据。代价函数在搜索过程中可以动态地改变。v 如果代价函数是固定的，则相当于散开搜索法。如果代价函数是固定的，则相当于散开搜索法。v 目前，被证明有用的代价函数或定向表达式还不多见。目前，被证明有用的代价函数或定向表达式还不多见。 第第5章章 协议验证技术协议验证技术 算法二：受控部分搜索算法算法二：受控部分搜索算法v 概率搜索法。概率搜索法。v 在这种方法中，根据状态出现的概率的递减顺序来选择后在这种方法中，根据状态出现的概率的递减顺序来选择后继状态。将系统中的所有变迁都

46、标上标签，最简单地处理继状态。将系统中的所有变迁都标上标签，最简单地处理就是打上就是打上“高或高或“低标签，分别表示出现概率的高低。低标签，分别表示出现概率的高低。然后，根据标签来选择要检查的状态。然后，根据标签来选择要检查的状态。 v 随机选择法。随机选择法。v 前几种方法总是试图预测在何处最容易发现协议错误，这前几种方法总是试图预测在何处最容易发现协议错误，这种预测是有很大风险的。种预测是有很大风险的。v 因为根据因为根据Murphy定律的推论，错误最可能隐藏在设计者定律的推论，错误最可能隐藏在设计者或验证者认为不像有错误的地方或验证者认为不像有错误的地方Holz93。v 随机选择法不关心

47、在哪些状态最可能发现错误，而是随机随机选择法不关心在哪些状态最可能发现错误，而是随机地选择后继状态。地选择后继状态。v 它不仅是一种最容易实现的技术，也是一种最有可能产生它不仅是一种最容易实现的技术，也是一种最有可能产生高质量的搜索的方法。高质量的搜索的方法。 第第5章章 协议验证技术协议验证技术 算法二：受控部分搜索算法算法二：受控部分搜索算法v一般来说，受控部分搜索算法较全局搜索方法有一般来说，受控部分搜索算法较全局搜索方法有效和可行。但是，这种方法不能保证协议无错。效和可行。但是，这种方法不能保证协议无错。通常需要执行多次才能得到比较可信的结果。通常需要执行多次才能得到比较可信的结果。

48、第第5章章 协议验证技术协议验证技术 算法三：随机模拟算法算法三：随机模拟算法v 前面介绍的受控部分搜索算法部分地解决了穷尽性可达性前面介绍的受控部分搜索算法部分地解决了穷尽性可达性分析算法的状态爆炸问题，因而得到了广泛的应用。分析算法的状态爆炸问题，因而得到了广泛的应用。 v 但是，在有些情况下，这种受控部分搜索算法也会变得不但是，在有些情况下，这种受控部分搜索算法也会变得不可行。例如，如果想直接将一个协议验证算法应用到一个可行。例如，如果想直接将一个协议验证算法应用到一个高度详细的、正在一台机器上运行的、经编译过的代码上高度详细的、正在一台机器上运行的、经编译过的代码上时，即使是使用受控部

49、分搜索算法也需要大量的内存来保时，即使是使用受控部分搜索算法也需要大量的内存来保存搜索的状态。存搜索的状态。 v 在这种情况下，惟一可行的方法是从搜索算法中去掉状态在这种情况下，惟一可行的方法是从搜索算法中去掉状态集集A A和和W W，而用随机模拟，而用随机模拟(random simulation)(random simulation)或随机遍历或随机遍历(random walk)(random walk)的方法搜索协议的状态空间。的方法搜索协议的状态空间。 第第5章章 协议验证技术协议验证技术 算法三：随机模拟算法算法三：随机模拟算法analyze() /* 随机模拟随机模拟 */ q =

50、初始状态初始状态; while (1) if (q = 错误状态错误状态) report_error(); q = 初始状态初始状态; else q = q的一个后继状态；的一个后继状态；第第5章章 协议验证技术协议验证技术 三种算法的比较三种算法的比较v 穷尽性可达性分析算法的优点在于可以证明协议中没有错穷尽性可达性分析算法的优点在于可以证明协议中没有错误，但问题在于其应用范围有限。误，但问题在于其应用范围有限。v 最主要原因是该算法能分析的最大状态数目依赖于协议、最主要原因是该算法能分析的最大状态数目依赖于协议、描述方法和可用的计算资源。特别是当系统状态的数目非描述方法和可用的计算资源。特

51、别是当系统状态的数目非常大时会发生状态空间爆炸。常大时会发生状态空间爆炸。v 一般来说，根据协议状态空间大小和可用的内存空间，这一般来说，根据协议状态空间大小和可用的内存空间，这种算法的覆盖率并不一定能达到种算法的覆盖率并不一定能达到100%100%。如果状态空间大小。如果状态空间大小为为R R，执行搜索时内存中能够存储的最大状态数为，执行搜索时内存中能够存储的最大状态数为A A，那么，那么只有当只有当R R小于等于小于等于A A时覆盖率和搜索质量才能达到时覆盖率和搜索质量才能达到100%100%。 v 当当R R大于等于大于等于A A时，全搜索策略将变成部分搜索，且不能保时，全搜索策略将变成

52、部分搜索，且不能保证检查协议中最重要的部分，覆盖率减小到证检查协议中最重要的部分，覆盖率减小到A/RA/R，而搜索质，而搜索质量变得更差。量变得更差。v 因此，对于复杂的协议，穷尽性可达性分析的效果只能算因此，对于复杂的协议，穷尽性可达性分析的效果只能算作是一种低质量的部分搜索。作是一种低质量的部分搜索。 第第5章章 协议验证技术协议验证技术 三种算法的比较三种算法的比较 (Cont.)v 受控部分搜索算法的目的是证明错误的存在，而不是证明受控部分搜索算法的目的是证明错误的存在，而不是证明没有错误。没有错误。v 与穷尽性可达性分析相比，这种算法可以有效地解决状态与穷尽性可达性分析相比，这种算法

53、可以有效地解决状态空间爆炸问题，同时利用有限的资源来验证协议的最重要空间爆炸问题，同时利用有限的资源来验证协议的最重要的部分，从而最大限度地发现错误。的部分，从而最大限度地发现错误。v 其缺点是必须能够预先判断出协议中的错误的大概位置，其缺点是必须能够预先判断出协议中的错误的大概位置，然而这很难预先做到。由于，多个进程间的关系非常复杂，然而这很难预先做到。由于，多个进程间的关系非常复杂，不能仅仅根据其表面的关系来判断。不能仅仅根据其表面的关系来判断。v 另外，虽然这些方法能够减小状态空间的大小，但它们都另外，虽然这些方法能够减小状态空间的大小，但它们都没有提供任何工具，将状态空间的大小与可用内

54、存相匹配。没有提供任何工具，将状态空间的大小与可用内存相匹配。v 使用这些方法时，有效搜索的部分状态空间的大小是协议使用这些方法时，有效搜索的部分状态空间的大小是协议相关的，只能通过实验确定，要想找到一种最优的方法，相关的，只能通过实验确定，要想找到一种最优的方法，必须按照不同的选择策略进行多次验证。必须按照不同的选择策略进行多次验证。 第第5章章 协议验证技术协议验证技术 三种算法的比较三种算法的比较 (Cont.)v 随机模拟算法与协议系统的大小和复杂性无关，即使随机模拟算法与协议系统的大小和复杂性无关，即使是无限大小的系统，也可以应用。因此，对于复杂的是无限大小的系统，也可以应用。因此，

55、对于复杂的验证问题，这种算法也许是唯一可用的方法。验证问题，这种算法也许是唯一可用的方法。v 但这种方法也有些问题，例如，但这种方法也有些问题，例如，v 它没有明确的终止，无法判断是否已经访问过系统的它没有明确的终止，无法判断是否已经访问过系统的所有可达状态；所有可达状态；v 由于没有算法的终止，也就无法判断是否已经发现了由于没有算法的终止，也就无法判断是否已经发现了系统的所有错误系统的所有错误v 因此只能发现协议中的错误，而不能证明协议中没有因此只能发现协议中的错误，而不能证明协议中没有错误。错误。 第第5章章 协议验证技术协议验证技术 可达性分析可达性分析三、基于可达性分析的协议错误的检测

56、方法三、基于可达性分析的协议错误的检测方法 第第5章章 协议验证技术协议验证技术 协议错误的检测协议错误的检测v死锁。死锁。v如果一个状态无任何后继状态，那么该状态就是如果一个状态无任何后继状态，那么该状态就是死锁状态。死锁状态。v无意义事件。无意义事件。v在穷尽可达性分析中，如果一个事件未被执行一在穷尽可达性分析中，如果一个事件未被执行一次，那么该事件可判定为无意义事件。次，那么该事件可判定为无意义事件。v对于非穷尽可达性分析，算法在执行一遍之后，对于非穷尽可达性分析，算法在执行一遍之后，如果某些事件未执行一次，那么在第二遍执行中如果某些事件未执行一次，那么在第二遍执行中应将这些事件的优先级

57、别数值提高。只有当非穷应将这些事件的优先级别数值提高。只有当非穷尽可达性分析进行多次之后，才能判定哪那些事尽可达性分析进行多次之后，才能判定哪那些事件为无意义事件。件为无意义事件。 第第5章章 协议验证技术协议验证技术 协议错误的检测协议错误的检测Cont.）v 非确定的输入事件。非确定的输入事件。 v 如果某个协议实体在执行输入事件之后所获取的报文不是如果某个协议实体在执行输入事件之后所获取的报文不是它所期待的报文，那么这个事件为非确定输入事件。非确它所期待的报文，那么这个事件为非确定输入事件。非确定输入事件反映协议的完整性不好，即协议没有考虑异常定输入事件反映协议的完整性不好，即协议没有考

58、虑异常报文的接收处理问题。报文的接收处理问题。 v 活锁。活锁。 v 活锁的检测首先是循环的检测。当所有循环都已检测出来活锁的检测首先是循环的检测。当所有循环都已检测出来之后，我们就可以判定那些循环是死循环。之后，我们就可以判定那些循环是死循环。 v 死循环的判定是较为复杂的问题。一种方法是通过死循环的判定是较为复杂的问题。一种方法是通过“进展进展状态状态(progress state)(progress state)”的标记来确定一个循环是否为死的标记来确定一个循环是否为死循环。如果循环序列之内包含致少一个进展状态，那么它循环。如果循环序列之内包含致少一个进展状态，那么它就不是死循环。进展状

59、态的标记在可达性分析进行之前由就不是死循环。进展状态的标记在可达性分析进行之前由手工进行。手工进行。 v 例如：发送例如：发送-超时超时-再发送再发送 构成一个循环，如果发送之构成一个循环，如果发送之前判定发送次数是否超过给定数值前判定发送次数是否超过给定数值( (超过就转向错误处理超过就转向错误处理) )，那么再发送状态就可以标记为进展状态。那么再发送状态就可以标记为进展状态。 第第5章章 协议验证技术协议验证技术 可达性分析可达性分析四、状态空间爆炸问题四、状态空间爆炸问题 第第5章章 协议验证技术协议验证技术 状态空间爆炸问题状态空间爆炸问题v随着协议复杂性的提高和队列通道边界值的增随着

60、协议复杂性的提高和队列通道边界值的增大，状态爆炸问题使穷尽可达性分析无法进行。大，状态爆炸问题使穷尽可达性分析无法进行。v除了前面介绍的部分搜索算法，还可以采用下除了前面介绍的部分搜索算法，还可以采用下列方法来减小状态空间使之处于一个可控制的列方法来减小状态空间使之处于一个可控制的范围之内。范围之内。 v部分规格说明和验证部分规格说明和验证(Partial Specification (Partial Specification and Verification) and Verification) v选择大的动作单元选择大的动作单元(Choosing Large Units of (Choo