计算机网络通信协议验证技术的研究.pdf
《计算机网络通信协议验证技术的研究.pdf》由会员分享,可在线阅读,更多相关《计算机网络通信协议验证技术的研究.pdf(3页珍藏版)》请在淘文阁 - 分享文档赚钱的网站上搜索。
1、协议是网络的血液和生命,计算机网络的发展是网络协议设计和开发的结果。但计算机通信与网络技术的发展进一步增强了协议的复杂性,主要体现在协议开发难度大、周期长、而且潜在错误多,而协议开发过程中任何一点错误和缺陷都将给分布系统的稳定性、可靠性、坚固性、安全性、容错性以及异种系统之间互通性带来巨大的危害。为此,便出现了协议工程。协议工程用形式化的方法描述在协议严格的设计和维护中的各个活动,它是研究以对象为协议的软件工程,但所建立的协议设计方法比现有软件工程的一般方法更严格,从而使协议开发整个过程一体化、系统化和形式化。协议工程包括形式化描述、协议验证、协议综合、协议实现、协议一致性测试等多方面的理论和
2、技术。在这些形式化技术中,形式化描述与验证技术是整个协议设计与实现的基础,对协议实现的正确性、完整性和复杂度有至关重要的影响。协议验证技术的目的与方法1 对协议本身的逻辑正确性进行校验的过程称之为验证。协议验证有两种途径:协议分析和协议综合,通常所说的协议验证指的是前者。协议分析的目的是:对已设计的协议进行分析和校验 这些已设计的协议大都是采用非形式化设计(方法产生的。)协议的正确性验证试图在协议开发的前期最大限度地检测和纠正协议错误和缺陷,包括死锁、活锁、不可执行的行动、协议外部性能不符合服务要求等。协议验证技术多种多样但可以分为类:可达性分析是最常用的技术,它包括状态穷举、状态随机枚举、状
3、态概率枚举等方法;逻辑证明试图用推理演算方法严密的证明协议各种性质,采用的推理演算技术主要来自与时序逻辑、谓词逻辑、代数演算等数学领域;第三类验证技术是模拟。协议综合将协议设计和协议验证紧密结合起来,也可以认为是一类验证技术。基于网的协议验证与分析2 Petri一组通信实体可以描述为单一的或成组的相互通信的网模型,网间通信由直接耦合或者由库所和变迁表示的Petri通道实现。网络的动态特性如控制和数据流由发生规则和标记分布描述。为适应不同规范及验证的需求,从基本网Petri模型衍化出许多扩展模型系统,如谓词 动作网、时间/Petri网、带时态逻辑的网、有色网Petri(TPN)Petri Pet
4、ri、面向对象网等。网还没有国际标(XCPN)Petri(NPN)Petri准,但已得到广泛应用,其优越性表现在:采用图表(1)示,清晰直观;具有很好的适应性,不仅能适应计算机(2)科学而且也适应于社会、物理等领域;它能描述系统的(3)并发行为,使用网的分析技术对模拟系统进行分析,能Petri得到系统行为方面的信息;具有坚实的数学基础和分析(4)技术。对于单个特定协议的验证可能涉及专门的技术,而可达性分析和不变量分析是验证大多数协议的基本途径,网Petri模型的许多性质都可以由它们推导出来,这为映射相应协议的性质提供了可能。而网自身具备的可运行性方便了系Petri统形式化描述级模拟。可达性分析
5、是指生成网的全部可达状态,以检查是否符(1)Petri合协议所要求出现的状态以及期望的行为特征,通常包括死锁、意外接收 发送、变迁活性以及库所标记数的有界性等。可达性分析/从初始全局标识开始,根据每一个点活变迁或并发变迁集 同时具(备点火条件的变迁的集合 生成分支结点,总体上形成可达图。)不变量分析是要求网在特定执行模式下不变量的特性。(2)Petri研究最广泛且理论上最完备的两种不变量是不变量和不变量。T-P-不变量对应于网中标记总数保持不便的库所子集,它反映协P-Petri议的守衡性,如协议中的发送方、信道和接收方的缓冲器Stop-Wait中的报文总数恒为。不变量是指保持网标识不变的变迁序
6、列,1T-它反映协议运作的循环或重复特性。状态爆炸问题。由于状态空间随着模型增长,人们一直试图(3)压缩或网的规范。目前主要有保持特性变换和构造 分解理RGPetri/论这两种途径。前者的具体方法是,在保持有界性、活性等网Petri模型特性的前提下,增加生成可达图时的限制条件或在可达性分析作者简介:李艳,(1978)女,硕士生,主要研究方向为计算机网络管理与分布式系统;彭熙 ,硕士生;肖德宝,博导收稿日期:2001-10-22 计算机网络通信协议验证技术的研究李艳,彭熙,肖德宝 (华中师范大学计算机网络与通信研究所,武汉)430079摘要:协议设计、开发的复杂性的增加导致了协议工程技术的出现,
7、该文主要介绍了协议工程活动中的协议验证与分析阶段,阐述了验证技术的目的与方法,分析了当今常用的协议模型技术,重点介绍了基于网、以及时序逻辑模型的协议验证技术。PetriFMSTL关键词:计算机网络;协议;协议工程;协议验证;网PetriStudy on the Protocol Verification of Computer etwork,LI Yan,PENG XiXIAO Debao(Computer Science Department of Central China Normal University,Wuhan 430079)【】AbstractThe rapid increas
8、ement of protocol complexity results in a discipline of protocol engineering.This paper mainly introduces the protocol verification and analysis of protocol engineering activities,expounds the purpose and method of protocol verificatin,then analyzes the protocol model technology in common use,and in
9、troduces the protocol verification based on Petri Nets,FMS and TL model.【】Key words;Computer networkProtocolProtocol engineeringProtocol verificationPetri nets第卷第期2811Vol.28 11计算机工程Computer Engineering年月200211 November 2002开发研究与设计技术 中图分类号:TP 393.04 文章编号:10003428(2002)11 025102文献标识码:A 251之前间接地改变网模型,如
10、用单个库所或变迁代替一个特定子网,建立层次化的可达图或网模型以及基于等价关系削减结点数等。后者的关键问题是如何确定构造和分解网的规则,手段仍然是划Petri分子网,分析网元素的相关性以及建立层次模型等。其他分析功能。由于网具备严格的矩阵运算理论支持,(4)Petri它还能推导出许多系统行为特征,如等价关系、进程等;而网Petri与其他几种形式化描述工具的内在联系使得它能起到模型间的桥梁作用,已经出现许多自动正向 反向翻译网与或/PetriEstelleLOTOS 等语言工具。这里要特别提到的是,因为数学基础是随机过程 排(队论,所以,能够用于协议的性能评价,定量地求解系统的主)SPN要性能指标
11、,如报文队列长度 库所标记数、吞吐量和丢包率等。()基于有限状态自动机模型的协议验证与分析3 有限状态机是最为重要的一种形式描述技术,它是FSM很多形式化方法的基础。它直观性强,可实现与其它形式方法的组合和转换,且易于自动实现,因而在中占有重要FDT的地位。有限状态机最常用的技术是可达性分析技术。可达性分析技术试图产生和检查协议所有或部分可达状态。所谓可达性状态指协议从状态开始经历有限次转换之后达到的状态,所有可达性状态构成可达图。可达性分析最重要的工作是产生和检查可达图,判断是否存在死锁、活锁等协议错误,它涉及 个重要技术:怎样找出所有可达图,构成可3(1)达图;怎样检测死锁、活锁等协议错误
12、;怎样解决状(2)(3)态爆炸问题。一般来说,对于每次发生的转变,可通过使用系统全局状态来决定特性,像是否表示一个死锁状态,所有实体是否在当前状态能接收发给它的所有报文等。基于描述的协议验证可通过构造可达树来实现。可FSM达树的根为系统的初始状态。从初始状态出发,列举出全部可能的转移,每一个转移将产生一个新的状态空间,即形成可达树的一个叶节点,产生一个叶节点的过程叫一次扰动过程。在此叶结点的基础上,不断生长新的叶节点,直到没有新的叶节点为止。可达树上各节点分别表示某一给定时刻的全局状态矩阵,它动态地反映了两个或多个协议实体(GMS)或进程的交互活动。由于简单、直观而得到广泛应用,FSM但不利于
13、协议验证的实现,不易于描述复杂的系统。基于时序逻辑的协议验证与分析4 基于模态逻辑的研究4.1 这种逻辑包含各种关于对分布式系统中消息的知识和信任,或从某些知识得到其他知识和信任的推倒规则。最有影响的逻辑系统则属,和于Burrows MAbadi MNeedham R1989年提出的逻辑BAN1。逻辑形式化定义协议的目标,并BAN且还确定了协议初始时刻各参与者的知识和信任,通过协议里消息的发送和接收步骤产生新知识,使用推导规则来得到目标信任和知识。如果得到最终的关于知识和信任的语句集里不包含所要得到的信任和知识语句时,就表明协议存在安全缺陷。逻辑包含 个推导规则,基本上能表达信任的BAN5建立
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 计算机网络 通信协议 验证 技术 研究
限制150内