随着计算机网络、通信网络以及分布式系统的不断发展,通信协议有日渐复杂化的趋势,形式描述技术在网络协议设计中占有举足轻重的作用,作为国际化标准之一的LOTOS技术是专为分布式系统设计的形式描述技术,特别是通信服务和协议。 本文对LOTOS技术在网络通信协议设计中的应用方法进行了研究。归纳总结了基于LOTOS的形式化描述方法、形式化的转换、验证和实现等方法理论,以及通信服务和协议的构造方法及服务规范到协议规范的等效性转换方法,重点研究了规范风格和结构概念及渐进细化设计方法在服务和协议设计中的应用。 文章主要由四部分构成: 第一部分:简要介绍了形式描述技术在协议工程中的应用范围,LOTOS技术的背景和发展状况(第一章);然后介绍了LOTOS的语言基础(第二章)。 第二部分:详细描述了在网络协议设计中基于LOTOS相关技术的应用领域及在这些领域中的应用方法,包括:LOTOS规范风格、LOTOS转换、LOTOS验证、LOTOS实现、ELOTOS以及LOTOS工具集等(第三章)。 第三部分:详细论述了通信模型的构造方法,服务规范和协议规范的构造方法,及将服务规范转变为协议规范的方法(第四章)。 第四部分:提出了LOTOS规范风格在网络服务和协议设计中的应用方法、形式结构模型的概念及实现方法、渐进细化设计方法、LOTOS规范的C、C++实现方法(第五章);提出渐进细化设计方法,并举一案例说明基于LOTOS的网关协议的系统设计(第六章)。