文摘
英文文摘
原创性声明和关于学位论文使用授权的说明
第一章绪论
1.1课题的研究背景
1.1.1协议工程概述
1.1.2形式化描述技术概述
1.1.3研究基于LOTOS的形式描述技术的意义
1.2课题的应用背景
1.3课题研究的内容
第二章LOTOS基础
2.1 LOTOS技术概述
2.2 LOTOS中常用的基本概念
2.2.1进程及其相关概念
2.2.2门径
2.3行为算子
2.4抽象数据类型
2.4.1简单抽象数据类型的定义
2.4.2对已有类型的扩充或组合
2.4.3参数化类型的定义
2.4.4类型重命名
第三章基于LOTOS技术的应用
3.1 LOTOS规范风格(Specification Styles)
3.1.1整体的风格(Monolithic style)
3.1.2面向约束的风格(Constraint-oriented style)
3.1.3面向状态的风格(State-oriented style)
3.1.4面向资源的风格(Resource-oriented style)
3.2 LOTOS的转换
3.2.1形式化转换
3.2.2转换策略
3.3 LOTOS的实现
3.3.1目标实现环境
3.3.2实现空白
3.3.3抽象模型到实现模型
3.3.4最终实现规范实现(realising the implementation)
3.4 LOTOS的验证
3.4.1测试
3.4.2校验
3.5 LOTOS的扩展ELOTOS和ET-LOTOS
3.6 LOTOS协议工具集EUCALYPTUS
第四章服务和协议规范的构造方法
4.1 LTS和双向模拟
4.2通信模型
4.3规范构造方法
4.3.1两个实体的规范构造
4.3.2多实体规范构造
第五章结构概念与协议设计
5.1结构概念与规范语言
5.2等级抽象和渐进细化在规范描述中的应用
5.3形式结构模型的创建原则和方法
5.3.1设计形式结构模型所需遵守的原则
5.3.2形式结构模型的创建方法
5.4协议设计和规范风格在设计中的作用
5.5渐进细化的设计方法
5.6 LOTOS渐进细化设计方法在互斥访问系统中的应用
5.7 LOTOS规范的C、C++实现方法研究
5.7.1抽象数据类型的实现
5.7.2进程定义的实现
5.7.3规范定义的实现
5.7.4行为表达式的实现
第六章基于进程算子和LOTOS语言的网关协议的系统设计
6.1渐进细化设计方法概述
6.2网关体系结构设计（GATEWAY ARCHITECTURE DEVELOPMENT）
6.2.1结构背景（ARCHITECTURAL BACKGROUND）
6.2.2功能选择（SELECTION OF FEATURES）
6.2.3网关结构的LOTOS描述（GATEWAY ARCHITECTURE SPECIFICATION IN LOTOS）
6.3参考体系结构设计（REFERENCE ARCHITECTURE DEVELOPMENT）
6.3.1功能分解标准（DECOMPOSITION CRITERIA）
6.3.2网关功能分解（THE GATEWAYDECOMPOSITION）
6.4进一步转换
6.4.1事件细化（EVENT REFINEMENT）
6.4.2交互点分解（INTERACTION POINT DECOMPOSITION）
6.5本章结论和展望
结论与展望
参考文献
致谢
攻读学位期间发表论文
