《协议验证技术》PPT课件

《《协议验证技术》PPT课件》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第5章协议验证技术内容提要概述1协议性质2可达性分析3不变性分析42协议验证Holzman：每一个新设计的协议在被完全证明没有错误之前，都应认为不是完全正确的。协议验证技术和形式描述技术是同步发展的，它也是协议工程技术中研究最早、最深入的课题，使用的技术方法多种多样。3验证的含义“验证”的含义：验证协议的设计。通过分析每一层的所有协议实体间的所有可能的交互、协议的抽象规范中所确定的功能以及通过低层提供的服务所实现的对等层间的通信来确定上述操作是否满足协议的服务规范。在设计阶段进行验证，可以及早发现协议错误，大大降低协议开发成

2、本。验证协议的实现。检查每一个协议实体的实现是否满足它的抽象协议规范。大多数情况下，协议实现的验证是通过不同的测试工具来实现的。有时也将其称为协议实现评估或协议的一致性测试一般情况下，协议验证指的是第(1)类验证，这也是本课程的观点。具体来说，协议验证是指根据协议规范来检查协议实体间的交互是否满足一定特性(properties)或条件(conditions)的过程，例如，检查是否有死锁存在。通过协议验证，可以获知协议设计是否满足正确性、完整性和一致性等要求。4VerificationandValidation在英文文献中，“

3、验证”一词有两种不同的表示：validation和verification。它们的含义也比较混乱。文献[Rud98]认为:validation主要是指检查协议逻辑上的一致性，以查实协议设计中是否存在某些错误，这些错误是所有协议中都可能存在的共性错误，与具体的协议功能无关，例如，验证有无死锁。而verification则是指检查协议是否能成功地提供指定的协议功能。文献[Lai98]认为:verification主要是指检查一个系统是否满足它的规格说明，而validation的含义则不仅包括verification，还可能包括对

4、最终的系统实现进行测试，系统模拟，性能分析预测等。5VerificationandValidationBohem：Verification:toestablishthetruthofcorrespondencebetweenasoftwareproductanditsspecification(“truth”)orarewebuildingtheproductright?Validation:toestablishthefitnessorworthofasoftwareproductforitsoperationalmiss

5、ion(“tobeworth”)orarewebuildingtherightproduct?谢94版网络书中介绍：Verification:在功能方面进行验证Validation:在语法方面进行证实在实践当中，validation和verification所采用的技术并没有明显的界限。也正因为如此，很多文献并没有严格区分validation和verification，而是混用这两个单词。6VerificationandValidation7形式化验证非形式化验证则主要通过传统的遍历(walkthrough)和代码检查(in

6、spection)来实现。协议验证通常与形式描述技术有关。形式化验证主要将形式描述技术和推理技术相结合，是形式化描述技术的一个重要方面，其优点是：一方面可以获得无二义性的协议规范，另一方面可以通过计算机辅助工具来帮助实施自动或半自动验证。协议设计者必须在早期的协议设计阶段采用一些技术或工具来发现设计中存在的错误，这也是协议验证的最重要的目的。8形式化协议验证主要两类方法：模型检测（ModelChecking）：基于状态搜索（StateExploration）演绎验证（DeductiveVerification）：基于定理证明

7、（TheoremProving）9模型检测方法步骤：建模（Modeling）描述（Specification）验证（Verification）问题：状态空间爆炸协议运行的无穷状态空间的不可搜索性协议运行过程中的无穷消息空间的不可搜索性10定理证明方法步骤：将实现方案和功能描述都转换为一种形式逻辑，如命题逻辑、一阶逻辑（FirstOrderLogic,FOL）、高阶逻辑（HigherOrderLogic,HOL）等建立公理系统，作为验证的依据，并将协议性质构造成一组代定数定理根据公理系统，使用定理证明器，通过逻辑推理、逻辑规约

8、等手段，构造证明过程，证明实现方案和功能描述等价问题：入门难，前两步难11内容提要概述1协议性质2可达性分析3不变性分析412协议性质协议验证的最主要内容是检查协议是否满足规定的协议性质。一般情况下，将协议性质分为两类：一般性质(generalproperties)。指所有协议所具有的一些