资源描述：
《基于fsm的通信协议形式描述与验证技术_李腊元》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、系统工程与电子技术1990年第9期基于FSM的通信协议形式描述与验证技术武汉水运工程学院李腊元摘要本文主要研讨基子有限状态机(FsM)的通信协议形式描述与验证技术。文中先论述,了基本FSM形式描述与验证技术给出了访问确认协议的FSM描述与验,证实例研讨了基于FSM验证方法的形式数学基础全局状态矩阵的特征和性质;FS;最—。接着讨论了基于M的有关改进形式技术后给出了有关结论主题词计算机网络,数据通信,通信法规,规程3.混合模型,包括转移模型与程序语、一引言言模型的相关组合,以及笔者建议的一种基于FSM、CS
2、P和抽象数AD据类型(T)的.近年来,随着计算机网络与分布式系统的混合模型等l3]。,.不断发展通信协议有日渐复杂化的趋向。为4其它模型和方法,包括代数说明、、、使通信协议设计具有正确性完整性和安全时态逻辑跟踪模型(Trane)和维也纳开,,。性并使之易于验证和实现必须不断开发和发方法(VDM)等,完善通信协议的形式化技术提高协议设计的在形式描述语言的标准化方面也已获得。。、规范化和理论化程度所谓协议的形式化技术长足的进展150已相继推出Estele、主要是指协议及服务规范的形式描述协议的Lotos;CC
3、ITT早已建议并在不断地完善设计验证、实现验证和一致性测试,这已成为SDL。在协议的设计验证方面,主要有逻,、网络与分布式系统领域中一个十分重要的研究辑分析包括可达性分析象征性执行和程,。,。课题越来越引起人们的关注和兴趣关于形序正确性证明以及模拟仿真等技术协议,。式描述技术(FDT)目前已出现四类形式模的实现验证主要包括各种一致性测试技术型和方撼尹:目前,协议形式化技术的新趋向有以下几点1.转移模型,包括各种有限状态(自值得注意:动)机(FSM或fSA),各种Petri网,形1.完善150和CCITT建
4、议的标准形,,。。式文法L系统UCLA图等式语言及工具.,,.2程序语言模型包括类Pascal通2研究协议的软件规范和开发环境。信顺序进程(CSP),通信演算系统。CS)以及有关的逻辑语言等收稿:19904月23日(C日期年—40—.3研制相应的快速原型工具和各种自端。状态1为系统的初始状态,状态2为访,。、动工具。问请求状态状态3为访问就绪状态正4.开发协议描述和验证器及其机助协负号后面尾随的数目字表示报文,其中l号,,议设计与验证工作站以及其它的自动化系报文表示访问请求2号报文表示拒绝访统。问,3号报
5、文则表示访问确认(允许),4号,。,在通信协议的形式化技术中FSM由于报文表示中断访问当系统启动时进程Pl,。,直观性强可实现与其它形式模型组合和转和p:均处于初始状态在状态1下pl若,,。,,换且易于自动实现因而占有重要地位要请求访问则发送l号报文给几然后本文旨在研讨基于FSM的形式化技术。进人访问请求状态(状态2)。处于状态l:。的p在收到1号报文后也进人状态2此、,,二FSp:可有两种转移选择基本M形式化技术时其一是通过向Pl,,2号报文以拒绝p,的访问请求发送尔;p,一个有限状态机是一个五元组后返
6、回初始状态其二是可通过向发送,,,。,,A二(x1,0Nx是一个有3以响应或确认p,的访问请求川其中号报文限状态集,即状态数目是有限的。在网络和尔后进人一个新的状态(状态3)。类似,、,,分布式系统环境下状态可理解为发送接地处在状态2的p也可有两种转移选收、空闲或等待含义。I是一个输人集,它择,其一是当p:拒绝其访问请求时,则接,。,:可为一个有限集也可构成无限集输人信收p发送的2号报文尔后返回初始状,。,口;p:息与时间有关它可由报文来表征是态其二是当响应其访问请求时则接,。:,一有限输出集其有关规则与
7、I相似N是收p发送的3号报文尔后进人状态3o,,p,和p:3时p,和p:一个状态转移函数它由同一个时刻的输人当均处于状态都只,。l信息及前一个时刻的状态决定亦即存在一能有一种转移选择p将4号报文发送给几。,,:x一);p:l个映射(NIXX)M是一个输出函后返回初始状态接收到p发送的4数,输出信息可以看成是输人信息及状态的号报文后也将返回初始状态。。t函数它由t时刻的输人信息及时刻的状,卜态决定亦即存在一个映射(M:xXI‘O)。有限状态机可采用状态转移图,状态转移表或状态转移矩阵等形式来表示川。一211
8、+1.访FS问确认协议的M描述实例,在FSM模型中一个进程均可用一个通信有限状态机或一个有向标号图(状态转移图)来表征。图中的节点或圆圈表示状.,。态边或有向弧表示转移转移可以是报文,发送(用负号标记)也可以是报文接收图1访问确认协议(用正号表示)。每对进程可用一条全双工无.差错的FIFO通道进行连接。下面,我们给2全局状态矩阵分析。基于FSM描述的协议验证可通过构造出一个访问确认协议的FSM描述实例该。协议的状态转移图如图1
