基于时态逻辑的协议RSL形式化描述  

Formal Description of Protocols with RAISE Specification Language Based on Temporal Logic

作　　者：顾翔[1] 邱建林[1] 

机构地区：[1]南通大学计算机科学与技术学院,江苏南通226019

出　　处：《计算机工程》2011年第5期7-9,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60773041);江苏省高校自然科学基础研究基金资助项目(08KJB520009);南通市应用研究计划基金资助项目(K2008005);江苏省博士后科研资助计划基金资助项目(1002002B);江苏省高校"青蓝工程"基金资助项目

摘　　要：研究以RAISE规范语言(RSL)描述时态逻辑中always算子、sometimes算子和until算子的方法以及对复合时态算子的描述方法,提出在时态逻辑模型基础上用RSL对协议进行形式化描述的步骤,以AB协议为示例,给出其基于时态逻辑模型的RSL描述,从而证明该描述模型有利于协议验证和协议测试用例生成的自动实现。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.

关 键 词：时态逻辑 RAISE规范语言 形式化描述 协议工程 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]