基于RSL的协议形式化描述方法研究

摘要

协议工程是一体化、形式化的协议开发过程。协议的开发主要包括了协议设计、协议描述、协议验证、协议实现、协议测试和协议维护等过程。这里“一体化”的含义就是：协议开发的各个过程在技术上前后衔接，并在同一个开发系统中完成。“形式化”则指的是：用形式化描述语言FDL连接协议开发的各个阶段。
　　 在协议工程中，形式化描述技术占据了核心地位，它贯穿于整个开发过程的始终，因而它也是这一领域的研究热点。目前已有的一些协议形式化描述模型主要有：基于状态机的各类FSM、各类PetriNet，基于进程代数的CCS、CSP，时序逻辑TL等等。协议形式化描述语言则主要有Lotos、Estelle、SDL等。由于各种方法在协议描述与分析时有着各自的优、缺点，目前还没有一种方法能够完全满足协议工程的需要。
　　 本文所要研究的是基于RSL的协议形式化描述技术，将RSL引入协议工程领域。作为RAISE规范语言的RSL在进行协议描述时有着两个独有的优点：广谱性，这使得在进行协议描述时可以根据需要进行合理的抽象，从而在各个开发阶段，都可以使用RSL，使整个开发过程处于同一语义框架之下；描述手段的丰富与灵活，在使用RSL进行协议描述时，可以根据需要选用合适的语义模型，以最充分的表达协议内容与协议性质。
　　 本文的研究工作主要集中在以下三个方面：首先对RSL进行添加。RSL中缺乏时间描述机制，这是在协议描述中必须解决的一个问题。本文设计了两个方案对其进行添加。一个是引入时间类型Time和系统辅助函数System Time。该方案的优点在于Time是RSL固有类型Nat的子类型，它的引入不会影响到RSL原有的语法、语义架构和证明系统，缺点在于对描述的可读性和广谱性有所影响。一个是引入wait表达式。该方案的优点在于可读性强，缺点在于它的引入影响了RSL原有结构，需要对引入后RSL的语法、语义进行讨论。RAISE提供的工具也要进行相应的修改。然后用改进后的RSL对协议进行描述。改进后的RSL有着较丰富的描述手段和较强的描述能力。能够适用多种语义模型。本文研究了两类最基本的模型一基于状态机模型和基于进程模型的描述方法。在实际描述中，可以灵活的综合使用这两类模型。本文还讨论了一种基于输入/输出动作序列的描述方法。在协议描述的研究中，本文还针对RSL的特点，尝试了将面向对象的思想引入到描述中去。最后，以RIP协议的简化路由算法为实际示例，使用RSL对其进行了描述。

目录

文摘

英文文摘

声明

1引言

1.1背景介绍

1.2形式化描述技术现状

1.3内容与安排

2 RSL语言语言时间描述机制的添加

2.1 RSL语言综述

2.2 RSL规范的语法结构

2.3 RSL语言时间描述机制的添加

2.4改进后的RSL核心语法

2.5操作语义

2.6小结

3 RSL与协议形式化描述技术

3.1RSL的协议描述能力

3.2基于状态机模型的描述方法

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

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

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

3.6小结

4RIP协议路由算法的RSL描述

4.1 RIP协议简介

4.2 RIP协议的RSL描述

4.3小结

5结束语

致谢

参考文献

攻读学位期间发表的学位论文目录