协定验证 _生活百科

协定验证【协定验证】协定验证是指根据协定规範来检查协定实体间的互动是否满足一定特性(properties)或条件(conditions)的过程，例如，检查是否有死锁存在。通过协定验证，可以获知协定设计是否满足正确性、完整性和一致性等要求。
基本介绍中文名：协定验证
外文名：protocol verification
目的：对协定进行分析和校验
途径：协定分析和协定综合
工具：算法语言
领域：协定工程
概述对协定本身的逻辑正确性进行校验的过程称之为协定验证（protocol verification）。协定验证有两种途径：（1）协定分析（protocol analysis）（2）协定综合（protocol synthesis）通常所说的协定验证指的是前者。协定综合将协定设计过程和协定验证(分析)过程融合在一起，它通过一组能确保所设计的协定是正确的规则，从一些基本协定模组中（这些基本模组已证明是正确的）产生所希望的目标协定。协定分析的目的是：对已设计的协定进行分析和校验（这些已设计的协定大都是採用非形式化设计方法产生的）协定分析包括许多方法，例如，（1）可达性分析（reachability analysis）（2）不变性分析（invariance analysis）（3）等价性分析（equivalence analysis）（4）符号执行（symbol execution）、模拟（simulation）等等。这些分析工作可以手动完成。协定有多种表达形式，这包括：用自然语言描述的非形式化协定文本；用形式描述语言（ESTELLE，LOTOS,SDL等）描述的协定规範；用协定模型技术（FSM，Petrinet，CCS等）表达的协定模型；以及用程式设计语言（C，Pascal等）描述的协定代码。协定分析可在任何一种表达形式上进行，一般地说，上述所有方法都可在这几种表达形式上进行（手工或软体工具）。然而，除符号执行之外，人们都在协定模型上进行协定分析。这里介绍三种分析方法，它们是可达性分析、不变性分析和等价分析。可达性分析可达性分析是最常用的协定验证方法。它试图产生和检查协定所有或部分可达状态。“可达状态”是指协定从初始状态开始经历有限次转换之后可达到的状态。所有可达状态构成可达图(RG: Reachability Graph) 。可达性分析的原理是：採用穷举法检查同一层内两个或多个协定实体间所有可能的互动所产生的状态。将协作的协定实体的状态以及连线这些协定实体的低层称为系统的全局状态或混合状态(composite or global state) 。从一个给定的初始状态开始，所有可能的变迁(用户命令、逾时、报文到达等)产生许多新的全局状态。对每一个新产生的状态重複执行上述过程直到没有新的状态产生(某些变迁将导致系统返回到已产生的状态) 。对于一个给定的初始状态和一组关于低层协定的假定(提供的服务的类型)，这种分析能够确定协定可能产生的所有结果。可达性分析最适合于用状态变迁模型描述的协定模型。对于状态变迁模型的全局状态空间的产生也比较容易自动化，目前已有很多作此用途的工具。对于程式语言描述的协定模型也可以使用可达性分析方法。具体做法是：在程式中设定许多断点(break points)，这些断点有效地定义了系统的控制状态。不变性分析如果一个系统的某个性质能用一个确定的逻辑表达式描述，并且恆为真（不随系统的状态变化或执行序列而改变），那幺这个性质称为系统的不变性质，简称系统不变性。协定的不变性分析包括二个工作：第一是完全正确地找出系统（协定）的不变性质。形成严格定义的不变性表达式；第二是以某种方式执行协定，验证不变性表达式是否恆为真。我们所说的不变性分析指的是第二项工作。第一项工作由手工进行，许多协定描述文本也包含了不变性表达式。不变性分析可採用两种途径：第一是不变性证明系统（往往採用归纳法），第二是不变性监测系统。下面分别介绍它们。不变性证明系统採用归纳法时，协定不变性证明包括两步：验证协定处于初始状态时不变性表达式是否成立；然后，假定协定在某状态下不变性成立，验证协定从这个状态开始执行所有相关事件过程中不变性是否保持成立。不变性监测系统不变性监测系统藉助监测软体和监测方法对模拟运行或符号执行中的协定进行不变性校验的过程称之为不变性监测(invariant monitoring) 。这种方法要求在协定代码中插入断点(子程式的调用或返回可视为自然断点)，每个断点处，监测系统取相关变数值，计算并校验不变性表达式是否成立。通过监测系统进行不变性分析时，还会遇到一个麻烦问题：协定系统由多个协定实体组成(分布性)，监测系统必须凌驾于它们之上，实现起来比较困难。不变性监测程式还可对程式断言(assert)进行校验，程式断言是嵌于协定代码指定地方的特殊语句，例如ASSERT(state = =1) 。协定代码运行到ASSERT语句时将指示监测程式对ASSERT语句所申明的布尔表达式进行校验。不变性表达式则要求无论系统(协定)处于何种状态，不变性表达式都必须成立。此外，不变性表达式不同于程式断言之处还在于它无需插入协定代码中。等价性分析“等价”意味着某种程度上的“相同”和“无差别” 。如果两个协定模型或协定规範是等价的，那幺它们可以互相替换，如果一个是正确的，那幺另一个也是正确的。等价性分析的另一个途径是证明两个协定的FSM图或CCS表达式是等价的，典型的情况是证明协定规範和它的服务规範一致性。等价性分类如下：按等价的含义和等价的强弱，等价性分为：观察等价（observational equivalence）：如果对两个协定进行状态到状态的互相模拟时所观察到的协定行为没有差别，这两个协定是观察等价的。测试等价（test equivalence）：如果对两个协定施加相同的测试序列所观察到的协定行为没有差别，那幺这两个协定是测试等价的。跟蹤等价（trace equivalence）：如果两个协定执行的事件序列是相同的，那幺它们是蹤迹等价的。实现等价（implementation equivalence）：如果一个协定所做的每一件事情都能被第二个模仿（mimic），反之亦然，那幺它们是实现等价的。这四种等价按强弱程度排列的话，顺序是：观察等价、测试等价、跟蹤等价、实现等价，其中观察等价还分为强观察等价和弱观察等价。等价性的强弱反映两个协定对行为细节的相同程度，等价性越强，它们的行为细节的相同程度越高。协定性质协定验证的最主要内容是检查协定是否满足规定的协定性质。一般情况下，将协定性质分为两类：一般性质(general properties) 。指所有协定所具有的一些公共特性。不同文献对这类性质的个数和描述也不尽相同。特殊性质(specific properties) 。是指与具体协定内容有关的性质。对这些性质的定义构成了服务规範的主体内容。一般性质可达性(Reachability)：验证协定的各种可能状态之间的可达关係。如果协定的某个状态从初态不可达，则表明协定有错误。如果从状态A到状态B的变迁不可能发生(直接或间接)，则从状态A到状态B是不可达的。没有死锁(Deadlock freeness)：最典型的死锁是协定中各实体都处于这样的一种等待状态，即只有在“某一事件”发生后才能做进一步的动作，但在该状态下，这个“某一事件”却不可能发生。死锁发生时，协定所处的状态称为死锁状态。没有活锁(Livelock freeness) ：活锁是指协定处于无限的死循环中，而没有别的事件可使协定从这一循环中解脱出来。例如，协定无限制地执行逾时重发操作，但总是收不到对方的确认信息。状态还是在变化的，不过不能脱离这种死循环状态而已。弱活锁(Weak livelock)：是指协定处于死循环中，只有当协定交换命令的相对速度达到某一状态时，协定才退出死循环。时间相关的活锁(Time-dependent livelock)：也称为临时阻塞(Tempo-blocking) 。它是指协定处于死循环中，但是当通信双方交换报文的相对速度到达某一状态时，协定可以从死循环中出来。有界性(Boundedness)：检验协定的某些成分或参数的容量(例如：通道容量、视窗大小)是否有界。有界性是针对协定元素性质和通道性质而言。可恢复性或自同步性（Recovery from failures）：这是当出现差错后，协定能否在有限的步骤内返回到正常状态(包括初始态)执行。无状态二义性(State ambiguities freeness)：一个进程在某一时刻只允许具有一个稳定状态。所谓稳定状态是指当通信双方的通道为空时的进程状态。若在某一时刻进程可以有多个稳定状态，则称该进程的状态为二义状态。互斥性(Mutual exclusion)：互斥性是指有些协定动作不能同时被多个用户执行。例如，多个用户不能同时请求同一资源。终止或进展(Termination or Progress)：是指协定提供的服务必须在有限时间内完成。终止是针对终止协定(terminating protocols)而言，意思是指协定总是能到达期望的结束状态。而进展则是针对循环协定(cyclic protocols)而言，意思是指协定总是能到达它的初始状态。无冗余描述(Absence of Overspecification)：协定规範中没有无用的、冗余描述，例如，没有未经实践的报文接收(absence of unexercised message receptions) 。公平性(Fairness)：是指每一个协定实体均应平等地得到运行的机会，无论其它的协定实体想做什幺。特殊性质完整性(Completeness) 。是指协定设计考虑了所有可能发生的事件、选项以及服务。检验协定是否能处理所有可能的输入，即是否缺少套用的处理，或有无非期待的接收或输入(即错收) 。一致性(consistency) 。是指协定服务行为(或性质)和协定行为(或性质)一致，即协定应该提供用户要求的服务，而无需提供用户没有要求的服务。