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等）描述的协议规范；用协议模型技术（FSM，Petrinet，CCS等）表达的协议模

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

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

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

6、eachsuccessorstatesofqif(sisnotinAorW){addstoW;analyze();}deleteqfromW;}}第五章协议验证技术1.状态表示方法协议状态用状态矩阵表示为:这里E1，E2…，En，为n层协议的几个协议实体的局部状态，Cij为协议实体i到协议实体j的通道的状态。当所有通道可处理成空通道时，协议状态可用数组[E1,E2,…,En]表示（因为空通道只有一种状态）。第五章协议验证技术2.怎样找到所有可达的后继状态不考虑报文顺序号，AB协议系统如图5.1所示，其中C12是S到R的通道，C21是R到S的通

7、道，协议状态由二维矩阵组成。初始状态有四个后继状态：很显然，状态（2），（3）和（4）不是可达状态(因为初始状态中AB内部没有任何数据需要传输，所以（2），（3），（4）状态是不可能出现的，即不可达的)。那么怎样判定（1）是可达状态，而（2），（3）和（4）不是可达状态呢？第五章协议验证技术图5-1AB协议系统第五章协议验证技术为了解决这个问题，我们按下述格式定义交互事件：entity(state):action-point(state)?/!message这里，entity(state)表示协议实体处于状态state中，action-poi

8、nt(state)表示作用点处于状态state中，！表示发送，？表示接收。作用点的状态定义为“0”或“1”。发送（！）结束后，状态为“1”；接收（？）结束后，状态为