基于RSL的协议形式化描述语言研究

摘要

该文所要研究的是基于RSL的协议形式化描述技术,这是第一次将RSL引入协议工程领域.作为RAISE规范语言的RSL在进行协议描述时有着两个独有的优点:广谱性,这使得在进行协议描述时可以根据需要进行合理的抽象,从而在各个开发阶段,都可以使用RSL,使整个开发过程处于同一语义框架之下;描述手段的丰富与灵活,在使用RSL进行协议描述时,可以根据需要选用合适的语义模型,以最充分的表达协议内容与协议性质.此外,RAISE为RSL提供了一些工具,这也为协议开发中的自动化工作提供了基础.该文的研究工作主要集中在以下三个方面:(1)对RSL进行扩充RSL中缺乏时间描述机制,这是在协议描述中必须解决的第一个问题.该文设计了两个方案对其进行扩充.一个是引入时间类型Time和系统辅助函数SystemTime.该方案的优点在于Time是RSL固有类型Nat的子类型,它的引入不会影响到RSL原有的语法、语义架构和证明系统,缺点在于对描述的可读性和广谱性有所影响.一个是引入wait表达式.该方案的优点在于可读性强,缺点在于它的引入影响了RSL原有结构,需要对引入后RSL的语法、语义进行讨论.RAISE提供的工具也要进行相应的修改.(2)使用扩充后的RSL对协议进行描述;扩充后的RSL有着较丰富的描述手段和较强的描述能力.能够适用多种语义模型.该文研究了两类最基本的模型一基于状态机模型和基于进程模型的描述方法.在实际描述中,可以灵活的综合使用这两类模型.该文还讨论了一种基于输入/输出动作序列的描述方法,这是该文中要讨论的协议测试序列生成方法的基础.(3)协议验证与协议测试序列生成;在使用扩充后的RSL对协议进行描述的基础上,该文对协议的验证与协议测试序列的生成进行了初步的探讨.此外,该文还以RIP协议的简化路由算法和N-S协议作为实际示例,使用RSL对其进行了描述.

目录

文摘

英文文摘

第一章绪论

1.1研究背景

1.2协议形式化描述技术研究现状

1.2.1形式化描述技术

1.2.2几种常用的形式化描述技术

1.3研究内容与写作安排

第二章RSL语言

2.1 RSL语言简介

2.1.1 RSL语言的特点

2.1.2 RSL语言的描述风格

2.1.3与Z语言和VDM语言的比较

2.2 RSL规范的基本语法结构

2.2.1 RSL的模块

2.2.2 RSL的说明

2.3 RSL语言的扩充

2.3.1 Time类型的添加

2.3.2计时器的描述

2.3.3 wait表达式的添加

2.3.4注释

2.4扩充后的RSL核心语法

2.5操作语义

2.5.1概念说明

2.5.2操作语义

2.6小结

第三章基于RSL的协议形式化描述

3.1扩充后RSL的基本协议描述能力

3.1.1六种协议元素的描述

3.1.2基于RSL形式化描述的一般方法

3.2基于状态转移语义模型的描述方法

3.2.1有限状态机

3.2.2基于状态转移语义模型的一般描述方法

3.2.3 AB协议

3.2.4AB协议的描述

3.3基于进程语义模型的描述方法

3.3.1通信顺序进程

3.3.2基于进程语义模型的一般描述方法

3.3.3 AB协议的描述

3.4基于输入输出动作的描述方法

3.5面向对象思想与RSL描述的结合

3.5.1 RSL对面向对象的支持

3.5.2面向对象的协议模型OOFSM

3.5.3 TFTP协议的描述

3.6小结

第四章基于RSL描述的协议验证与测试技术

4.1协议验证技术简介

4.2基于RSL描述的协议验证技术

4.2.1使用RSL进行协议验证的基本规则

4.2.2协议性质

4.2.3示例1：应答式协议的验证

4.2.4示例2：AB协议的验证

4.2.5协议验证技术小结

4.3协议的一致性测试技术研究

4.3.1协议的一致性测试

4.3.2基于FSM的测试序列生成方法

4.3.3基于输入输出变迁系统的一致性测试

4.4基于RSL描述的协议测试技术

4.4.1 δ动作的添加

4.4.2测试序列的生成法则

4.4.3关于生成法则的讨论

4.5小结

第五章RIP协议路由算法的RSL描述

5.1 RIP协议简介

5.2 RIP协议的RSL描述

5.2.1 RIP协议的报文描述

5.2.2 RIP协议简化路由算法

5.2.3简化路由算法的RSL描述

5.3小结

第六章密码协议的RSL描述

6.1密码协议简介

6.1.1信息安全与密码协议

6.1.2密码协议的结构

6.2 N-S协议

6.3 N-S协议的RSL描述

6.4小结

第七章结束语

7.1论文工作总结

7.1.1 RSL语言的扩充

7.1.2协议描述

7.1.3协议验证与测试

7.2进一步的工作

参考文献

致谢

读博期间撰写、发表的论文