摘要： 讨论使用RAISE规范语言(RSL)描述6种协议元素的方法。在RSL描述的基础上，借助操作符的运算规则、并行扩展规则和同步会合事件隐藏规则，对协议的相关性质进行验证，以一个简化的停止等待协议规范的描述和验证实例证明，与其他形式化方法相比，RSL表现出较强的描述能力。
关键词:
协议工程,
形式化描述,
RAISE规范语言,
协议验证
Abstract: This paper discusses the way to use RAISE Specification Language(RSL) to describe six kinds of protocol elements. Based on RSL description, it uses operation rules of RSL operators, expansion rule of parallel operation and hide rule of synchronous-communicating events to verify related properties of the protocol. Description and verification of a stopping-waiting protocol are presented as an example, which prove that compared with other formal methods, RSL has better description ability.
Key words:
protocol engineering,
formal description,
RAISE Specification Language(RSL),
protocol verification
中图分类号:
顾 翔;邱建林;邵浩然. 基于RSL的协议形式化描述与验证方法[J]. 计算机工程, 2009, 35(23): 41-43.
GU Xiang; QIU Jian-lin; SHAO Hao-ran. Protocol Formal Description and Verification Method Based on RSL[J]. Computer Engineering, 2009, 35(23): 41-43.