协议验证技术.ppt

《协议验证技术.ppt》由会员分享，可在线阅读，更多相关《协议验证技术.ppt（64页珍藏版）》请在三一办公上搜索。

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

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

3、ud98认为:validation主要是指检查协议逻辑上的一致性，以查实协议设计中是否存在某些错误，这些错误是所有协议中都可能存在的共性错误，与具体的协议功能无关，例如，验证有无死锁。而verification则是指检查协议是否能成功地提供指定的协议功能。文献Lai98认为:verification主要是指检查一个系统是否满足它的规格说明，而validation的含义则不仅包括verification，还可能包括对最终的系统实现进行测试，系统模拟，性能分析预测等。,Verification and Validation,Bohem：Verification:to establish the t

4、ruth of correspondence between a software product and its specification(“truth”)or are we building the product right?Validation:to establish the fitness or worth of a software product for its operational mission(“to be worth”)or are we building the right product?谢94版网络书中介绍：Verification:在功能方面进行验证Vali

5、dation:在语法方面进行证实在实践当中，validation和verification所采用的技术并没有明显的界限。也正因为如此，很多文献并没有严格区分validation和verification，而是混用这两个单词。,Verification and Validation,形式化验证,非形式化验证则主要通过传统的遍历(walkthrough)和代码检查(inspection)来实现。协议验证通常与形式描述技术有关。形式化验证主要将形式描述技术和推理技术相结合，是形式化描述技术的一个重要方面，其优点是：一方面可以获得无二义性的协议规范，另一方面可以通过计算机辅助工具来帮助实施自动或半自动

6、验证。协议设计者必须在早期的协议设计阶段采用一些技术或工具来发现设计中存在的错误，这也是协议验证的最重要的目的。,形式化协议验证,主要两类方法：模型检测（Model Checking）：基于状态搜索（State Exploration）演绎验证（Deductive Verification）：基于定理证明（Theorem Proving）,模型检测方法,步骤：建模（Modeling）描述（Specification）验证（Verification）问题：状态空间爆炸协议运行的无穷状态空间的不可搜索性 协议运行过程中的无穷消息空间的不可搜索性,定理证明方法,步骤：将实现方案和功能描述都转换为一种

7、形式逻辑，如命题逻辑、一阶逻辑（First Order Logic,FOL）、高阶逻辑（Higher Order Logic,HOL）等 建立公理系统，作为验证的依据，并将协议性质构造成一组代定数定理 根据公理系统，使用定理证明器，通过逻辑推理、逻辑规约等手段，构造证明过程，证明实现方案和功能描述等价 问题：入门难，前两步难,内容提要,概述,1,协议性质,2,可达性分析,3,不变性分析,4,协议性质,协议验证的最主要内容是检查协议是否满足规定的协议性质。一般情况下，将协议性质分为两类：一般性质(general properties)。指所有协议所具有的一些公共特性。不同文献对这类性质的个数和描

8、述也不尽相同。特殊性质(specific properties)。是指与具体协议内容有关的性质。对这些性质的定义构成了服务规范的主体内容。也有文献将协议性质分为安全性(safety)和活跃性(liveness)。,一般性质,可达性(Reachability)。验证协议的各种可能状态之间的可达关系。如果协议的某个状态从初态不可达，则表明协议有错误。如果从状态A到状态B的变迁不可能发生(直接或间接)，则从状态A到状态B是不可达的。没有死锁(Deadlock freeness)。最典型的死锁是协议中各实体都处于这样的一种等待状态，即只有在“某一事件”发生后才能做进一步的动作，但在该状态下，这个“某一

9、事件”却不可能发生。死锁发生时，协议所处的状态称为死锁状态。没有活锁(Livelock freeness)。活锁是指协议处于无限的死循环中，而没有别的事件可使协议从这一循环中解脱出来。例如，协议无限制地执行超时重发操作，但总是收不到对方的确认信息。状态还是在变化的，不过不能脱离这种死循环状态而已。,一般性质（Cont.）,弱活锁(Weak livelock)。是指协议处于死循环中，只有当协议交换命令的相对速度达到某一状态时，协议才退出死循环。时间相关的活锁(Time-dependent livelock)。也称为临时阻塞(Tempo-blocking)。它是指协议处于死循环中，但是当通信双方交

10、换报文的相对速度到达某一状态时，协议可以从死循环中出来。有界性(Boundedness)。检验协议的某些成分或参数的容量(例如：通道容量、窗口大小)是否有界。有界性是针对协议元素性质和通道性质而言。可恢复性或自同步性（Recovery from failures）。这是当出现差错后，协议能否在有限的步骤内返回到正常状态(包括初始态)执行。,一般性质（Cont.）,无状态二义性(State ambiguities freeness)。一个进程在某一时刻只允许具有一个稳定状态。所谓稳定状态是指当通信双方的通道为空时的进程状态。若在某一时刻进程可以有多个稳定状态，则称该进程的状态为二义状态。互斥性(

11、Mutual exclusion)。互斥性是指有些协议动作不能同时被多个用户执行。例如，多个用户不能同时请求同一资源。终止或进展(Termination or Progress)。是指协议提供的服务必须在有限时间内完成。终止是针对终止协议(terminating protocols)而言，意思是指协议总是能到达期望的结束状态。而进展则是针对循环协议(cyclic protocols)而言，意思是指协议总是能到达它的初始状态。,一般性质（Cont.）,无冗余描述(Absence of Overspecification)。协议规范中没有无用的、冗余描述，例如，没有未经实践的报文接收(absenc

12、e of unexercised message receptions)。公平性(Fairness)。是指每一个协议实体均应平等地得到运行的机会，无论其它的协议实体想做什么。,特殊性质,完整性(Completeness)。是指协议设计考虑了所有可能发生的事件、选项以及服务。检验协议是否能处理所有可能的输入，即是否缺少应用的处理，或有无非期待的接收或输入(即错收)。也有的文献将完整性称为完全正确性(plete correctness)。一致性(consistency)。是指协议服务行为(或性质)和协议行为(或性质)一致，即协议应该提供用户要求的服务，而无需提供用户没有要求的服务。也有文献将一致性

13、称为部分正确性(partial correctness)、等价性(equivelence)等。,一般性质 vs.特殊性质,协议验证着重在于一般性质，而协议测试则着重于特殊性质。,安全性(safety)vs.活动性(liveness),安全性是指协议的所有动作均需与它的服务规范保持一致，即没有不期望的情况出现。不期望的情况包括：不可接收的事件、不可进一步向前的状态、错误的动作、错误的条件、变量值越界等。例如，如果传输协议传送报文，则它必须将这些报文传送到正确的目的地，按正确的顺序，并且无差错地交给目的主机。安全性保证协议不出现错误。活动性是指在有穷时间内，完成规范所规定的动作(或所有的服务必须在

14、有限时间内完成)。在进行逻辑验证时，确保一个有限的时延就足够了。但是，在验证协议的效率和响应能力时，则必须定量地确定期望的时延、吞吐率以及其它的一些指标。,安全性(safety)vs.活动性(liveness),活动性(Cont.)协议的活动性体现在终止性(termination)和进展性(progress)两个方面。终止性是指协议从任何一个状态开始运行，经过有限时间总能正确地达到终止状态；进展性是指协议从初始状态运行，经过有限时间总能到达指定状态。在某些情况下，终止状态和初始状态是同一的。这样，协议从初始状态出发总能正确地回到初始状态，并可反复运行。,内容提要,概述,1,协议性质,2,可达性

15、分析,3,不变性分析,4,协议验证方法,验证方法主要有两类：模型检查(Model Checking)。最常见方法：可达性分析(RA:Reachability analysis)，它包括状态穷举，状态随机枚举，状态概率枚举等方法 不变性分析(invariance analysis)等价性分析(equivalence analysis)重要问题：状态空间爆炸 证明(Proving)试图用推理演算方法严密地证明协议的各种性质其他方法：模拟（Simulation）通过一些模拟试验来测试协议的各种性质,可达性分析,一、概 述,可达性分析,可达性分析是最常用的协议验证方法。它试图产生和检查协议所有或部分可

16、达状态。“可达状态”是指协议从初始状态开始经历有限次转换之后可达到的状态。所有可达状态构成可达图(RG:Reachability Graph)。,可达性分析（Cont.）,可达性分析的原理是:采用穷举法检查同一层内两个或多个协议实体间所有可能的交互所产生的状态。将协作的协议实体的状态以及连接这些协议实体的低层称为系统的全局状态或混合状态(posite or global state)。从一个给定的初始状态开始，所有可能的变迁(用户命令、超时、报文到达等)产生许多新的全局状态。对每一个新产生的状态重复执行上述过程直到没有新的状态产生(某些变迁将导致系统返回到已产生的状态)。对于一个给定的初始状态

17、和一组关于低层协议的假定(提供的服务的类型)，这种分析能够确定协议可能产生的所有结果。,可达性分析（续）,可达性分析最适合于用状态变迁模型描述的协议模型。对于状态变迁模型的全局状态空间的产生也比较容易自动化，目前已有很多作此用途的工具。对于程序语言描述的协议模型也可以使用可达性分析方法。具体做法是：在程序中设置许多断点(break points)，这些断点有效地定义了系统的控制状态。可达性分析方法特别适用于验证上一节提到的协议的一般性质，因为这些性质是可达图结构的一种直接结果。没有出口的全局状态要么是死锁，要么是期望的结束状态。同样，收到一个没有定义如何处理的报文或超过了传输媒体的带宽等情况很

18、容易被发现。,可达性分析（Cont.）,可达性分析涉及三个重要技术：怎样找出所有可达状态，构成可达图。怎样检测死锁、活锁等协议错误。怎样解决状态空间爆炸问题。,可达性分析,二、可达性分析算法,可达性分析算法,文献Holz93给出了三个主要的可达性分析算法：穷尽性可达性分析算法(exhaustive or full search)，受控部分搜索算法(controlled partial search)，随机模拟算法(random simulation)。,算法一：穷尽性可达性分析算法,start()W=初始状态;/*工作集：分析的状态*/A=;/*已分析过的状态*/analyze();analy

19、ze()/*全局搜索*/if(W为空)return;q=取自W的元素；将q加入到A中 if(q是错误状态)report_error();/*报告错误*/else for(q的每一个后继状态s)if(s不在A或W中)把s加入到W中；analyze();从W中删除q；,工作集W控制系统状态空间树的搜索顺序。如果工作集W中的状态以先进先出（FIFO）的顺序取出，那么算法执行的是状态空间树的先广搜索（breadth-first）；如果以先进后出（FILO）的顺序取出，则是状态空间树的先深搜索(deapth-first)。先深搜索方法占用存贮空间小，这是其最大优点之一。,假定每个状态有两个后继状态，算法

20、执行m步之后，对于先深搜索方法，W的长度为m，而对于先广搜索方法，W的长度为2m。,算法一：穷尽性可达性分析算法,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；,算法一：穷尽性可达性分析算法,上述算法假定用来进行验证的计算机的存贮空间足够大，且计算速率足够高。这往往是不

21、现实的。因此，大多数情况下，只有将协议验证模型化简到给定机器能够分析的程度时基于这种算法的验证才可行。一般采用结构化或分层的方法来降低模型的复杂性。但在某些情况下，由于被分析的问题的固有复杂性，只能将模型化简到一定程度，因为如果再进一步化简则可能丢失其基本的、重要的性质。由此产生了另外一种搜索算法，即受控部分搜索算法。,算法二：受控部分搜索算法,/*start()与算法5.1中的相同*/analyze()/*部分搜索*/if(W为空)return;q=取自W的元素；将q加入到A中 if(q是错误状态)report_error();/*报告错误*/else for(q的某些后继状态s)if(s不

22、在A或W中)把s加入到W中；analyze();从W中删除q；,选择状态的规则有很多，例如，限制深度法(Depth-bounds)，散开搜索(Scatter Search)，定向搜索法(Guided Search)，概率法(Probabilistic Search)，启发式Yu91，随机选择法(Random Selections)West87，状态矢量法Holz91等,算法不考虑检查协议所有可能的状态，而是预先确定满足某些要求(如，死锁)的潜在的全局状态，然后检查这些状态是否可达。,算法二：受控部分搜索算法,限制深度法。原理是限制被分析的执行序列的长度，从而只需分析协议行为的一个子集。实质上，

23、限制了完全搜索算法中的工作集W的大小。限制深度法是一种相当标准和简单的部分搜索技术。散开搜索法。原理是尽可能选择有可能导致死锁的执行序列来进行检查，从而增加尽快发现错误的概率。例如，死锁的一个前提条件是没有待处理的报文(通道为空)，因此，这种算法更可能去检查报文接收操作而不是发送操作。定向搜索法。在定向搜索法中，为每一个后继状态计算它的代价函数值(cost function)。然后，根据这个计算结果作为是否执行它的依据。代价函数在搜索过程中可以动态地改变。如果代价函数是固定的，则相当于散开搜索法。目前，被证明有用的代价函数或定向表达式还不多见。,算法二：受控部分搜索算法,概率搜索法。在这种方法

24、中，根据状态出现的概率的递减顺序来选择后继状态。将系统中的所有变迁都标上标签，最简单地处理就是打上“高”或“低”标签，分别表示出现概率的高低。然后，根据标签来选择要检查的状态。随机选择法。前几种方法总是试图预测在何处最容易发现协议错误，这种预测是有很大风险的。因为根据Murphy定律的推论，错误最可能隐藏在设计者或验证者认为不像有错误的地方Holz93。随机选择法不关心在哪些状态最可能发现错误，而是随机地选择后继状态。它不仅是一种最容易实现的技术，也是一种最有可能产生高质量的搜索的方法。,算法二：受控部分搜索算法,一般来说，受控部分搜索算法较全局搜索方法有效和可行。但是，这种方法不能保证协议无

25、错。通常需要执行多次才能得到比较可信的结果。,算法三：随机模拟算法,前面介绍的受控部分搜索算法部分地解决了穷尽性可达性分析算法的状态爆炸问题，因而得到了广泛的应用。但是，在有些情况下，这种受控部分搜索算法也会变得不可行。例如，如果想直接将一个协议验证算法应用到一个高度详细的、正在一台机器上运行的、经编译过的代码上时，即使是使用受控部分搜索算法也需要大量的内存来保存搜索的状态。在这种情况下，惟一可行的方法是从搜索算法中去掉状态集A和W，而用随机模拟(random simulation)或随机遍历(random walk)的方法搜索协议的状态空间。,算法三：随机模拟算法,analyze()/*随机

26、模拟*/q=初始状态;while(1)if(q=错误状态)report_error();q=初始状态;else q=q的一个后继状态；,三种算法的比较,穷尽性可达性分析算法的优点在于可以证明协议中没有错误，但问题在于其应用范围有限。最主要原因是该算法能分析的最大状态数目依赖于协议、描述方法和可用的计算资源。特别是当系统状态的数目非常大时会发生状态空间爆炸。一般来说，根据协议状态空间大小和可用的内存空间，这种算法的覆盖率并不一定能达到100%。如果状态空间大小为R，执行搜索时内存中能够存储的最大状态数为A，那么只有当R小于等于A时覆盖率和搜索质量才能达到100%。当R大于等于A时，全搜索策略将变

27、成部分搜索，且不能保证检查协议中最重要的部分，覆盖率减小到A/R，而搜索质量变得更差。因此，对于复杂的协议，穷尽性可达性分析的效果只能算作是一种低质量的部分搜索。,三种算法的比较(Cont.),受控部分搜索算法的目的是证明错误的存在，而不是证明没有错误。与穷尽性可达性分析相比，这种算法可以有效地解决状态空间爆炸问题，同时利用有限的资源来验证协议的最重要的部分，从而最大限度地发现错误。其缺点是必须能够预先判断出协议中的错误的大概位置，然而这很难预先做到。因为，多个进程间的关系非常复杂，不能仅仅根据其表面的关系来判断。另外，虽然这些方法能够减小状态空间的大小，但它们都没有提供任何工具，将状态空间的

28、大小与可用内存相匹配。使用这些方法时，有效搜索的部分状态空间的大小是协议相关的，只能通过实验确定，要想找到一种最优的方法，必须按照不同的选择策略进行多次验证。,三种算法的比较(Cont.),随机模拟算法与协议系统的大小和复杂性无关，即使是无限大小的系统，也可以应用。因此，对于复杂的验证问题，这种算法也许是唯一可用的方法。但这种方法也有些问题，例如，它没有明确的终止，无法判断是否已经访问过系统的所有可达状态；由于没有算法的终止，也就无法判断是否已经发现了系统的所有错误因此只能发现协议中的错误，而不能证明协议中没有错误。,可达性分析,三、基于可达性分析的协议错误的检测方法,协议错误的检测,死锁。如

29、果一个状态无任何后继状态，那么该状态就是死锁状态。无意义事件。在穷尽可达性分析中，如果一个事件未被执行一次，那么该事件可判定为无意义事件。对于非穷尽可达性分析，算法在执行一遍之后，如果某些事件未执行一次，那么在第二遍执行中应将这些事件的优先级别数值提高。只有当非穷尽可达性分析进行多次之后，才能判定哪那些事件为无意义事件。,协议错误的检测（Cont.）,非确定的输入事件。如果某个协议实体在执行输入事件之后所获取的报文不是它所期待的报文，那么这个事件为非确定输入事件。非确定输入事件反映协议的完整性不好，即协议没有考虑异常报文的接收处理问题。活锁。活锁的检测首先是循环的检测。当所有循环都已检测出来之

30、后，我们就可以判定那些循环是死循环。死循环的判定是较为复杂的问题。一种方法是通过“进展状态(progress state)”的标记来确定一个循环是否为死循环。如果循环序列之内包含致少一个进展状态，那么它就不是死循环。进展状态的标记在可达性分析进行之前由手工进行。例如：发送-超时-再发送 构成一个循环，如果发送之前判定发送次数是否超过给定数值(超过就转向错误处理)，那么再发送状态就可以标记为进展状态。,可达性分析,四、状态空间爆炸问题,状态空间爆炸问题,随着协议复杂性的提高和队列通道边界值的增大，状态爆炸问题使穷尽可达性分析无法进行。除了前面介绍的部分搜索算法，还可以采用下列方法来减小状态空间使

31、之处于一个可控制的范围之内。部分规格说明和验证(Partial Specification and Verification)选择大的动作单元(Choosing Large Units of Actions)分解或划分(Deposition or Partitioning)按断言来分类状态(Classifying States by Assertions),部分规格说明和验证,根据具体描述方法的特点，只选取协议的某些方面进行描述。例如，在用状态变迁图来描述协议时，常常只描述主要状态间的状态变迁规则，而忽略参数值和其它的状态变量等细节。,选择大的动作单元,状态空间爆炸是因为不同实体执行的动作相互

32、交织所造成的。我们可以通过合并一些状态或动作来减少状态及变迁数。例如，可以将协议数据的准备和发送看作是一个不可分割的动作，从准备到发送不需同其它实体交互。从而可以将这样一个动作看作是一次“状态变迁”。这种方法的一个特殊应用例子是：仅仅考虑传输通道为空时的状态，即发送方发送的报文立即能够到达接收方。当要传输的报文的数量比较小或不考虑传输时延时，这种“空通道抽象”是合理的。在这种情况下，可以将不同实体的发送和接收变迁合并到一个涉及到两个实体的联合状态变迁中。,分解或划分,这种方法前提条件是可以将协议分解或划分成多个可控制的阶段、子层或模块。然后，对每一个子层、阶段或模块进行独立地描述和验证。由于分

33、解后的协议组件或阶段的状态及状态变迁数要远小于原始协议，所以这种方法大大降低了对原始协议验证的复杂性。例如，将HDLC分解成以下几个子层：比特填充、校验和过程元素。后者又可以细分为几个组件。需要注意的是，证明了每一个组件或阶段的正确性，并不一定能安全保证原始协议的正确性。,按断言来分类状态,在可达性分析中，考虑状态类而不是单个状态。通过选择合适的谓词，可以大大减少状态数目。例如，考虑一个协议实体接收编号的信息帧。不考虑将序列号变量的各种可能的值看作是不同的状态，取而代之仅仅考虑三种状态：变量“小于”，“等于”，“大于”收到的信息帧的编号。,内容提要,概述,1,协议性质,2,可达性分析,3,不变

34、性分析,4,不变性分析,如果一个系统的某个性质能用一个确定的逻辑表达式描述，并且恒为真(不随系统的状态变化或执行序列而改变)，那么这个性质称为系统的不变性质，简称为系统不变性(system invariance)。协议不变性分析包括二个工作：第一是完全正确地找出系统(协议)的不变性质，形成严格定义的不变性逻辑表达式。这项工作由手工进行，许多协议描述文本也包含了不变性表达式。第二是以某种方式执行协议，验证不变性表达式是否恒为真。我们所说的不变性分析指的是第二项工作。,不变性分析,不变性分析可采用两种途径：不变性证明系统(通常采用归纳法)；不变性监测系统。,不变性证明系统,采用归纳法时，协议不变性

35、证明包括两步：验证协议处于初始状态时不变性表达式是否成立；然后，假定协议在某状态下不变性成立，验证协议从这个状态开始执行所有相关事件过程中不变性是否保持成立。,不变性监测系统,不变性监测系统借助监测软件和监测方法对模拟运行或符号执行中的协议进行不变性校验的过程称之为不变性监测(invariant monitoring)。这种方法要求在协议代码中插入断点(子程序的调用或返回可视为自然断点)，每个断点处，监测系统取相关变量值，计算并校验不变性表达式是否成立。通过监测系统进行不变性分析时，还会遇到一个麻烦问题：协议系统由多个协议实体组成(分布性)，监测系统必须凌驾于它们之上，实现起来比较困难。由于上

36、述这些问题和原因，不变性分析在协议验证中的应用受到很大限制。,系统不变式 vs.断言,不变性监测程序还可对程序断言(assert)进行校验，程序断言是嵌于协议代码指定地方的特殊语句，例如ASSERT(state=1)。协议代码运行到ASSERT语句时将指示监测程序对ASSERT语句所申明的布尔表达式进行校验。不变性表达式则要求无论系统(协议)处于何种状态，不变性表达式都必须成立。此外，不变性表达式不同于程序断言之处还在于它无需插入协议代码中。,不变性分析：问题,无论是不变性证明系统还是监测系统，下述两个问题都是不可判定问题：不变性表达式已完整、准确、严密地表述了协议的所有行为和性质吗？用归纳法

37、证明不变性时，引用的原子操作已覆盖所有相关操作吗？在监测系统中，所设立的断点完备吗？,不变性分析：参考文献,Butler Lampson 在MIT的讲稿:“Principles of Computer Systems”,其他验证方法,协议综合(SYNT:Synthesis)协议综合通过构造设计规则来自动产生正确的协议。协议综合将协议设计和协议验证紧密结合起来。它力图使用一组能够确保所产生的协议是正确的规则，由“协议零部件”装配出一个符合要求的目标协议，或由协议的需求描述生成一个目标协议。这种方法常常采用交互式的规范和验证系统来保证所产生的规范的正确性。模拟(SIM:Simulation)模拟通

38、过协议规范的执行来获得协议行为的描述。这种方法一般用于复杂协议的验证。这些复杂协议的状态空间巨大，以致于很难用可达性分析来实施验证。一般的模拟只涉及到协议状态空间中的部分状态。如果模拟涉及到所有的状态，则相当于可达性分析，这种模拟称为穷尽性模拟(Exhaustive simulation)。,其他验证方法（Cont.）,规范执行(SPE:Specification Execution)如果协议规范是用可执行的规范描述语言写的，则可以通过执行协议规范来验证协议的性质。当然，规范执行需要一个语言解释器。在软件工程中，这种方法也称为快速原型(rapid prototyping)。混合方法(HT:Hy

39、brid Technique)就协议规范而言，可达性分析和程序证明两种方法的混合方法能够充分利用这两种技术的优点。用状态模型来描述协议的主要状态，从而使状态空间保持在比较小的水平，因而可以用一些自动分析方法来分析协议的一般性质。对于特殊性质，可以利用由变量和过程组成的断言的证明来处理。,验证技术功能比较,小结,问题：协议描述不精确使得验证结果不准确；协议实际特性比抽象出来的特性更加复杂；复杂协议通常还与加密算法和其它因素有关；协议的复杂性使得验证非常困难，此外信息的多样性很难考虑完全。,思考题,试分析滑动窗口协议，找出一到二个滑动窗口协议的不变式来。撰写一篇关于状态空间爆炸问题的综述文章。（参考文献98-4(StateSpaceExplosion).ps）5-25-35-45-5,