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

• 作者: 邱建林 顾翔
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 时态逻辑 RAISE规范语言 形式化描述 协议工程
• 年，卷（期）: 2011,（5）
• 页码范围: 7-9
• 分类号: TP311
• 字数: 3820字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2011.05.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	顾翔	南通大学计算机科学与技术学院	51	204	7.0	11.0
2	邱建林	南通大学计算机科学与技术学院	43	246	9.0	14.0