基于RSL的协议形式化描述与验证方法

Protocol Formal Description and Verification Method Based on RSL

讨论使用RAISE规范语言(RSL)描述6种协议元素的方法。在RSL描述的基础上,借助操作符的运算规则、并行扩展规则和同步会合事件隐藏规则,对协议的相关性质进行验证,以一个简化的停止等待协议规范的描述和验证实例证明,与其他形式化方法相比,RSL表现出较强的描述能力。

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.