下载掌阅APP，畅读海量书库
立即打开
协议形式化是指使用形式描述技术(FDT)贯穿于协议开发的各个阶段，使得协议的研究开发可以独立于非形式的自然语言文本和最终实现代码，避免协议验证、测试的复杂性。
网络通信系统具有状态多、行为复杂、与环境联系紧密等特点。形式化方法使得对网络通信系统的描述、实现和测试变得容易。系统行为的复杂性增大了行为描述的难度，人们必须借助一种语言或一种技术来准确地描述系统行为。在过去，人们习惯使用自然语言进行协议描述（用自然语言写协议的规格说明或规范），其优点是表达能力强、可读性好、方便，但缺点是不严格、不精确、结构不好、没有描述标准和有二义性，且从自然语言描述的协议到协议的实现一般要手工进行，很难进行协议实现、测试的自动化和协议验证。由于不同的人对协议描述的理解不一样，因此这样设计出的协议不但不能保证不同协议实现之间的互连，甚至还会得出错误的协议。例如，1978年版的X.25建议书中，对端到端序号的含义以及拆除连接等的意义都规定得不清楚，有二义性。
因此，需要采用协议形式化描述技术，它是准确获得协议规范的唯一方法。虽然采用形式描述的直接目的是为了得到协议的规范，但它还可带来下列好处：
（1）给协议开发提供坚实的基础，使用数学的方法不但能够提供无二义性的描述，而且能够对描述进行形式分析。
（2）支持协议工程活动的各个环节的实现和自动化，特别是协议综合、验证、自动实现（协议程序代码的自动生成）和一致性测试。利用数学技术开发描述语言的编译器和由描述派生的自动测试序列，将大大提高协议实现和维护的能力，降低提供和维持信息服务的代价。
用于协议的FDT一般应具有如下重要特性[12]：
完整的语法和语义定义。
体系结构、服务和协议的可表达性。
协议重要特性（如，无死锁）的可分析性。
支持复杂协议的管理（如，构造能力）。
支持逐步求精的方法。
支持实现独立性（包括并发性、非确定性和适当的抽象机制）。
支持协议生命期的各个环节，包括验证、实现和测试。
支持协议设计、验证、实现和维护过程的自动化或半自动化。
能准确地描述进程交互的各种原语。
我们将FDT分为两种类型：形式描述模型(FDM，Formal Description Model)和形式描述语言(FDL，Formal Description Language)。通过形式描述模型，可以获得抽象的协议模型。形式描述语言总是基于某一种或多种形式描述模型，也有形式化的语法和数学语义。从1968年起，人们研究了大量的形式描述技术，并且提出了各种描述协议的模型和语言。形式描述模型主要有：状态变迁模型，主要包括：有限状态机(FSM，Finite State Machine)模型、扩展的有限状态机(EFSM，Extended FSM)模型和Petri网模型；时序逻辑（或时态逻辑）（TL，Temporal Logic)；进程代数(Algebra of Process)，主要包括：通信系统演算(CCS，Calculus for Communication System)和通信顺序进程(CSP，Communicating Sequential Processes)等。在形式描述语言方面，国际标准化组织ISO和CCITT都非常支持用形式化方法来描述网络通信协议。目前已有三种主要的形式描述语言被标准化，它们是：SDL(Specification and Description Language)，LOTOS (Language Of Temporal Ordering Specification)和ESTELLE (Extended State Transition Language)。此外，ISO还制定了一些其他形式描述语言，如抽象语法记法(ASN.1，Abstract Syntax Notation One)和用来作为抽象测试集描述语言的TTCN(将在第7章介绍）。各种高级程序设计语言，如Pascal，PL/1，也属于形式描述语言
。用它们来描述协议的优点是便于协议的实现，但缺点是大多数高级程序设计语言比较复杂，分析起来比较困难，且不支持非确定性的描述。
实际应用时，往往将多种形式描述技术混合起来使用。例如，用状态变迁模型描述协议的最大优点是直观性好，同时也便于协议的验证。但是当协议比较复杂时，描述协议的图形也变得复杂起来，这就是所谓的状态空间爆炸问题。同时，状态变迁模型也不便于实现。高级语言则相反，有利于协议的实现，但在进行协议验证时则较困难。如果将这两种形式描述技术结合起来使用，将协议中的主要状态变迁用图形表示（有限状态机或Petri网），而协议的其他细节则用高级语言描述。这样就使得协议的描述和验证都比较方便。
本章简要介绍几种主要的协议模型，协议形式描述语言将在下一章详细介绍。