用于通信网络协议开发的形式化方法

【摘要】 随着形式化方法和技术日趋完善，网络协议开发也逐渐向形式化描述方法过渡和发展，并逐渐渗透到网络协议分析、综合及测试的各个环节中，形成应用于各个环节的软件工程方法。本文通过对通信网络协议的要素进行分析，并对网络协议形式化方法、形式化模型及描述进行阐述，在此基础上对通信网络协议的形式化方法进行了探究，并给出了一些自己的看法和建议。

【关键词】 通信网络协议 形式化方法 协议要素 描述技术

一、前言

随着计算机网络技术的不断发展及广泛应用，新一代的通信网络逐渐向着数字化、智能化和个人化发展，网络所提供的服务也开始由传统的通信服务逐渐向信息服务转变。随着软件的不断增多，结构越来越复杂，通信网络协议也面临着越来越多的困难。与此同时，网络系统在空间分布性、不稳定性及多样性方面表现出来的复杂性对通信网络协议的完整性、正确性、可靠性及标准化都提出了更高的要求。伴随着通信网络协议开发成本的增加，市场竞争的周期开始缩短，在通信网络协议的开发和设计上采用协议工程技术和方法，并有效实现通信网络设计合使用过程的规范化和自动化，成为当前通信网络协议开发课题中的热点及难点问题。本文就围绕着通信网络协议开发的形式化方法进行探究。

二、网络协议的要素分析

能够确保计算机网络顺利进行数据通信的通信网络协议，其要素主要包括以下几点：第一，网络协议所能提供的服务；第二，网络协议运行环境的假设；第三，实现网络协议的词汇信息及对每个词汇信息进行的编码；第四，控制消息保持一致性的规则。

能够在计算机之间实现网络数据通信自动化的协议，一般来说都是很复杂的，针对这种复杂的问题，采用分层结构来理解网路协议，具有重要作用。其中，“七层”协议结构模型是当前网络协议中的标准结构，是网络协议开发的基础。

三、网络协议形式化方法、形式化模型及描述

网络协议形式化方法是采用数学方法对目标软件的系统性质进行描述的一种技术方法。通过使用数学符号及数学法则就目标软件系统的结构来进行综合分析，研究，为网络协议的开发和验证提供一个利于发现目标软件和系统需求不完整性、不一致性等问题的框架。网络协议的形式化方法主要还是通过形式描述技术，即FDT技术来获得支持，形式化方法描述与模型技术及形式描述语言息息相关。

网络协议的形式化模式，其核心技术就是对协议进行分析和设计。形式化模型主要有以下几种：第一，有限状态机模型。这种模型主要在有限状态集、输入集和转移规则集，其中，有限状态集一般用于对系统不同状态进行描述；输入集则对系统接受的不同信息进行表征；状态转移规则集则主要是对表述系统在接受不同输入时，转移到下一个状态的规则。第二，Petri网模型，此种模型是适用于并发、异步及分布式系统描述和分析的数学工具，是目前网络协议中的典型模型之一，具有静态结构和动态行为机制。第三，协议时态逻辑模型，此种模型在时间信息的事件、状态及其关系命题中予以应用，对标识系统中的个体常量、定义变量等进行表达，进而对协议进行描述。

四、SDL

SDL产生于1976年，是由ITU-T发展的一种FDT，它是一种基于有限状态机建立的数学模型，用于事件驱动、实时和通信系统的描述语言。其形式化方法主要是作为对开发结果进行验证、测试的基础，为设计和应用人员提供交流的途径，进而为开发者提供一种分析、设计的方法。SDL着重从全局的视角来对系统结构进行描述，对系统中哪些是由子系统构成，各子系统之间如何相互作用等进行描述，进而递归式的对各子系统功能和结构进行描述。

SDL分为图形和文本两种形式，对系统功能进行说明，并对系统内部结构行为进行描述。纯文本表示更容易被计算机处理；而图形表示则更直观，利于进行可视化建模。SDL对一种层次结构来进行描述说明，其结构和功能并明确划分，功能块之间通过信道相连；同时，各个功能块还可以分为子功能块或进程。SDL对一些基本数据类型和操作以及对构造新的类型进行了定义，因此可以用于系统设计和实现。对SDL的优缺点而言，SDL能够通过全局视角，递归式的对各子系统功能及结构进行描述，并对硬件系统和其他各种人造或非人造系统进行描述。与此同时，SDL也具有一定的缺点，例如，SDL不适用于对需要大量进程的紧密协作，不能对并行处理和应用进行很好的处理；不能适应所有类型的实时系统等。

五、LOTOS

LOTOS产生于1989年，是用于详细说明和通信系统的描述技术标准形式，适应协议工程、分布处理及并行处理技术的要求，进而形成的规范语言，充分引入抽象的数据类型，对进程行为及交互作用进行描述。LOTOS主要是针对分布式的开放系统规范，尤其对开放式系统连接计算机网络架构的服务与协定，进行形式化的技术描述。LOTOS被用来对系统中事件发生顺序来建立运作模式，通过衍生自过程的运作模式和引入抽象数据形态结构来分析，提供对特定抽象数据形态的对等描述。LOTOS中的一个系统可以当做多个相互通信的进程；同时，这些进程又可以由多个子进程构成，进行一个规范的层次结构。一个进程通过门径和内部行为的时序关系来进行交互和定义；两个进程通过一个门径，可以对数值进行匹配，行程三种交互作用，这种进程行为为表达式描述。

六、ESTELLE

ESTELLE开始于1981年，由ISO发起，在1989年被批准为国际ISO标准，能够实现完整、一致、简练的描述分布，并对信息进行处理。ESTELLE使用的是Pascal语法和数据类型，基于扩展的通信有限状态机理论，在事件驱动行为建模中进行数据处理方面，能够准确描述并信息系统，因此，特别适合用于通信协议。ESTELLE是有许多相互通信的模块分层构成的系统，在每一级别中可以有多个模块，同时，每个模块和子模块中，都能通过通道以异步方式或凄然模块进行通信，而通道则是在两个实体之间相互传送的结构化双向路由。其本元素为模块，由模块头和模块体组成。其中，模块头被定义为外部交互点和输出变量。模块体则被定义为三个部分，即初始化部分，说明部分和跃迁部分。根据模块中是否包含状态变迁，可以分为三种类型，即活跃模块。目前，在ESTELLE中，已经开发看多个用于设计、调试、测试的工具，形成了一套完整的ESTELLE开发工具套。ESTELLE与SDL的扩展基本一致，但在某些概念上有所不同，ESTELLE扩展主要体现在：用变量和变量型的表示状态空间不一样；所用参数表示交互的方式不一样；操作与变迁相联系的方式也不一样。ESTELLE大部分主要集中在对ISO的应用协议进行描述。

七、Petri网

Petri网是在1962年，德国的Carl Adam Petri的博士论文中提出，是使用网状结构模拟通信系统，研究信息系统及其相互关系的数学模型，用于并发和分布系统行为描述的建模技术，目前，Petri网还没有明确的国际标准，但已经在分布式系统和通信协议的相关验证机性能分析反面得到了广泛应用。PN是对某一个系统状态及变化所提供的图形表达方式，通过可视描述功能，能够对模拟系统的动态和活动行为进行标记。一组通信实体能够被描述为单一的或相互通信的Petri网模型，由位置和跃迁表示通道实现，网络的动态特征，例如控制和数据流等由标记进行分布描述。为了适应不同协议的需求，Petri模型逐渐扩展到多个模型系统。近年来，Petri网技术得到了极大发展，各种网系统被开发，例如，条件/事件网，变迁网，有色网等，这些网络协同的开发对复杂系统的建模能力实现了很大的扩展作用。

Petri网对系统结构能够较好的描述，对系统中并发、同步、冲突及顺序等关系，可以用图形等来表示组合模型，更具有直观、易懂和易用的优势。Petri网具有严格定义的数学对象，具备完善的数学理论为基础。Petri网作为系统建模的工具，在系统设计和分析中，着眼于系统发生的变化，以及变化发生的条件和影响。因此，从组织结构的角度来看，其模拟系统不涉及系统所依赖的物理和化学原理；精确描述系统中事件的依赖关系与不依赖关系，这是事件之间的客观存在，也不依赖与观察的关系；Petri网还具有与应用环境无关的动态行为，作为可独立的研究对象，且Petri网可以在具有不同应用领域中得到不同的解释，进而起到沟通不同领域间桥梁的作用和效果。

八、结束语

形式化方法被用于描述复杂的系统，对通信系统的描述、实现和测试均变得十分容易，对此，在通信网络协议的开发设计中，就应该积极采用一些形式化的方法，在网络协议开发和使用效率及降低开发成本上做出贡献。

综上所述，通过对形式化方法在建模、验证及性能分析方面的比较，在对某些性质或协议工程的某些阶段的工作的秒速比较好，而在其他阶段和方面则表现出一些缺陷。例如，SDL在分析技术方面较为缺乏，LOTOS对于所描述的协议抽象性级别比较高，Petri网则在复杂语义和时序方面进行扩展的描述到具体实现的差距较大。由此可见，通信网络协议开发的形式化方法多有不同，尚没有一个完全泛用型的方法。因此，在对通信网络协议进行开发时就要在关键过程中引入形式化方法。

参考文献

[1]鲁来凤，吴振强，马建峰.基于PCL的改进型Helsinki协议的形式化分析[J].华中科技大学学报（自然科学版），2011（4）：34-36

[2]王惠斌.安全认证协议的设计与分析[D].信息工程大学，2010.11：111-113

[3]罗军舟.从Petri网到形式描述技术和协议工程.软件学报，2000，11（5）：606-615

[4]古天龙，蔡国永.网络协议的形式化分析与设计.北京：电子工业出版社， 2003，11（12）：54-57[5]潘红艳，于全.用于通信网络协议开发的形式化方法[J].计算机工程，2004，30（01）：129-131

[6]徐文超.网络协议的形式化分析与设计[J].信息技术，2012，11（02）：121-123