摘要： 研究以RAISE规范语言(RSL)描述时态逻辑中always算子、sometimes算子和until算子的方法以及对复合时态算子的描述方法，提出在时态逻辑模型基础上用RSL对协议进行形式化描述的步骤，以AB协议为示例，给出其基于时态逻辑模型的RSL描述，从而证明该描述模型有利于协议验证和协议测试用例生成的自动实现。
关键词:
时态逻辑,
RAISE规范语言,
形式化描述,
协议工程
Abstract: This paper researches how to use RAISE Specification Language(RSL) to describe operators of Temporal Logic(TL), such as always operator, sometimes operator, until operator and complex operators of TL, and presents the method of formal description with RSL based on TL model. Formal description of AB(Alternating Bit) protocol with RSL based on TL model is given as an example. The result proves that the description model helps realizing automatic implementation of protocols verification and testing.
Key words:
Temporal Logic(TL),
RAISE Specification Language(RSL),
formal description,
protocol engineering
中图分类号:
顾翔, 邱建林. 基于时态逻辑的协议RSL形式化描述[J]. 计算机工程, 2011, 37(5): 7-9.
GU Xiang, QIU Jian-Lin. Formal Description of Protocols with RAISE Specification Language Based on Temporal Logic[J]. Computer Engineering, 2011, 37(5): 7-9.