5 协议验证技术 (ok)

5 协议验证技术 (ok)

ID:20542307

大小:939.00 KB

页数:53页

时间:2018-10-13

5  协议验证技术 (ok)_第1页
5  协议验证技术 (ok)_第2页
5  协议验证技术 (ok)_第3页
5  协议验证技术 (ok)_第4页
5  协议验证技术 (ok)_第5页
资源描述:

《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”;接收(?)结束后,状态为

当前文档最多预览五页,下载文档查看全文

此文档下载收益归作者所有

当前文档最多预览五页,下载文档查看全文
温馨提示:
1. 部分包含数学公式或PPT动画的文件,查看预览时可能会显示错乱或异常,文件下载后无此问题,请放心下载。
2. 本文档由用户上传,版权归属用户,天天文库负责整理代发布。如果您对本文档版权有争议请及时联系客服。
3. 下载前请仔细阅读文档内容,确认文档内容符合您的需求后进行下载,若出现内容与标题不符可向本站投诉处理。
4. 下载文档时可能由于网络波动等原因无法下载或下载错误,付费完成后未能成功下载的用户请联系客服处理。