5 协议验证技术 (ok)

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

1、第五章协议验证（分析）技术5.1概述对协议本身的逻辑正确性进行校验的过程称之为协议验证（protocolverification）.协议验证有两种途径：（1）协议分析（protocolanalysis）（2）协议综合（protocolsynthesis）通常所说的协议验证指的是前者。协议综合（将在第六章讨论）将协议设计过程和协议验证(分析)过程融合在一起，它通过一组能确保所设计的协议是正确的规则，从一些基本协议模块中（这些基本模块已证明是正确的）产生所希望的目标协议。协议分析的目的是：对已设计的协议进行分析和校

2、验（这些已设计的协议大都是采用非形式化设计方法产生的）第五章协议验证技术协议分析包括许多方法，例如，（1）可达性分析（reachabilityanalysis）（2）不变性分析（invarianceanalysis）（3）等价性分析（equivalenceanalysis）（4）符号执行（symbolexecution）、模拟（simulation）等等。这些分析工作可以手动完成。协议有多种表达形式，这包括：用自然语言描述的非形式化协议文本；用形式描述语言（ESTELLE，LOTOS,SDL等）描述的协议规范；

3、用协议模型技术（FSM，Petrinet，CCS等）表达的协议模型；以及用程序设计语言（C，Pascal等）描述的协议代码。协议分析可在任何一种表达形式上进行，一般地说，上述所有方法都可在这几种表达形式上进行（手工或软件工具）。然而，除符号执行之外，人们都在协议模型上进行协议分析（简单，容易形成确定算法）。本章讨论三种分析方法，它们是可达性分析、不变性分析和等价分析。第五章协议验证技术5.2可达性分析可达性分析（基于FSM模型技术）试图产生和检查协议所有或部分可达状态。所谓可达状态指协议从初始状态开始经历有限次

4、转换之后可达到的状态，所有可达状态构成可达图（reachabilitygraph）.可达性分析的最重要工作是产生和检查可达图，判定是否存在死锁，活锁等协议错误。可达性分析涉及三个重要技术：（1）怎样找到所有可达状态，构成可达图；（2）怎样检测死锁、活锁等协议错误；（3）怎样解决状态爆炸问题。第五章协议验证技术5.2.1穷尽可达性分析穷尽（exhaustive）可达性分析产生和检查所有协议状态。算法5.1描述了穷尽可达性分析的基本算法，该算法假定计算机的存储空间足够大，计算速度足够高。第五章协议验证技术算法5.1

5、：exhaustivereachabilityanalysisstart(){W={initialstate};//工作集；将被分析的状态A={};//被分析过的状态analyze();//穷尽分析}analyze(){if(W==empty)return;q=lastelementfromW;集合W包含未被分析的协议状态，A包含已分析和正在分析中的协议状态,算法执行之前，W包含initialstate,A为空，算法执行完毕之后,W为空，A包含协议的所有可达状态。该算法简单明了，然而要将它付诸实施时,我们还必须

6、解决以下一些问题。addqtoA;findallsuccessorssofq;if(q==error_state)report_error();else{foreachsuccessorstatesofqif(sisnotinAorW){addstoW;analyze();}deleteqfromW;}}第五章协议验证技术1.状态表示方法协议状态用状态矩阵表示为:这里E1，E2…，En，为n层协议的几个协议实体的局部状态，Cij为协议实体i到协议实体j的通道的状态。当所有通道可处理成空通道时，协议状态可用数组[

7、E1,E2,…,En]表示（因为空通道只有一种状态）。第五章协议验证技术2.怎样找到所有可达的后继状态不考虑报文顺序号，AB协议系统如图5.1所示，其中C12是S到R的通道，C21是R到S的通道，协议状态由二维矩阵组成。初始状态有四个后继状态：很显然，状态（2），（3）和（4）不是可达状态(因为初始状态中AB内部没有任何数据需要传输，所以（2），（3），（4）状态是不可能出现的，即不可达的)。那么怎样判定（1）是可达状态，而（2），（3）和（4）不是可达状态呢？第五章协议验证技术图5-1AB协议系统第五章协议验

8、证技术为了解决这个问题，我们按下述格式定义交互事件：entity(state):action-point(state)?/!message这里，entity(state)表示协议实体处于状态state中，action-point(state)表示作用点处于状态state中，！表示发送，？表示接收。作用点的状态定义为“0”或“1”。发送（！）结束后，状态为“1”；接收（？）结束后，状态为