第4讲_协议验证技术

《第4讲_协议验证技术》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、网络协议工程第4讲：协议验证技术9/20/20211协议验证技术第4讲：协议验证技术4.1概述4.2协议性质4.3可达性分析4.4不变性分析4.5逻辑证明4.6其它验证方法9/20/20212协议验证技术协议验证每一个新设计的协议在被完全证明没有错误之前，都应认为不是完全正确的。协议验证技术和形式描述技术是同步发展的，它也是协议工程技术中研究最早、最深入的课题，使用的技术方法多种多样。9/20/20213协议验证技术验证的含义“验证”的含义：验证协议的设计。通过分析每一层的所有协议实体间的所有可能的交互、协议的抽象规范中所确定的功能以及通过低层提供的

2、服务所实现的对等层间的通信来确定上述操作是否满足协议的服务规范。在设计阶段进行验证，可以及早发现协议错误，大大降低协议开发成本。验证协议的实现。检查每一个协议实体的实现是否满足它的抽象协议规范。大多数情况下，协议实现的验证是通过不同的测试工具来实现的。有时也将其称为协议实现评估或协议的一致性测试一般情况下，协议验证指的是第(1)类验证，这也是本课程的观点。具体来说，协议验证是指根据协议规范来检查协议实体间的交互是否满足一定特性(properties)或条件(conditions)的过程，例如，检查是否有死锁存在。通过协议验证，可以获知协议设计是否满足正

3、确性、完整性和一致性等要求。9/20/20214协议验证技术VerificationandValidation在英文文献中，“验证”一词有两种不同的表示：validation和verification。它们的含义也比较混乱。文献[Rud98]认为:validation主要是指检查协议逻辑上的一致性，以查实协议设计中是否存在某些错误，这些错误是所有协议中都可能存在的共性错误，与具体的协议功能无关，例如，验证有无死锁。而verification则是指检查协议是否能成功地提供指定的协议功能。文献[Lai98]认为:verification主要是指检查一个系统

4、是否满足它的规格说明，而validation的含义则不仅包括verification，还可能包括对最终的系统实现进行测试，系统模拟，性能分析预测等。9/20/20215协议验证技术VerificationandValidationBohem：Verification:toestablishthetruthofcorrespondencebetweenasoftwareproductanditsspecification(“truth”)orarewebuildingtheproductright?Validation:toestablishthefit

5、nessorworthofasoftwareproductforitsoperationalmission(“tobeworth”)orarewebuildingtherightproduct?谢书中介绍：Verification:在功能方面进行验证Validation:在语法方面进行证实在实践当中，validation和verification所采用的技术并没有明显的界限。也正因为如此，很多文献并没有严格区分validation和verification，而是混用这两个单词。9/20/20216协议验证技术VerificationandValidat

6、ion9/20/20217协议验证技术形式化验证非形式化验证则主要通过传统的遍历(walkthrough)和代码检查(inspection)来实现。协议验证通常与形式描述技术有关。形式化验证主要将形式描述技术和推理技术相结合，是形式化描述技术的一个重要方面，其优点是：一方面可以获得无二义性的协议规范，另一方面可以通过计算机辅助工具来帮助实施自动或半自动验证。协议设计者必须在早期的协议设计阶段采用一些技术或工具来发现设计中存在的错误，这也是协议验证的最重要的目的。9/20/20218协议验证技术第4讲：协议验证技术4.1概述4.2协议性质4.3可达性分析

7、4.4不变性分析4.5逻辑证明4.6其它验证方法9/20/20219协议验证技术协议性质协议验证的最主要内容是检查协议是否满足规定的协议性质。一般情况下，将协议性质分为两类：一般性质(generalproperties)。指所有协议所具有的一些公共特性。不同文献对这类性质的个数和描述也不尽相同。特殊性质(specificproperties)。是指与具体协议内容有关的性质。对这些性质的定义构成了服务规范的主体内容。也有文献将协议性质分为安全性(safety)和活跃性(liveness)。9/20/202110协议验证技术一般性质可达性(Reachab

8、ility)。验证协议的各种可能状态之间的可达关系。如果协议的某个状态从初态不可达，则表明协议