李新宇

【摘要】 隨著形式化方法和技術日趨完善，網絡協(xié)議開發(fā)也逐漸向形式化描述方法過渡和發(fā)展，并逐漸滲透到網絡協(xié)議分析、綜合及測試的各個環(huán)節(jié)中，形成應用于各個環(huán)節(jié)的軟件工程方法。本文通過對通信網絡協(xié)議的要素進行分析，并對網絡協(xié)議形式化方法、形式化模型及描述進行闡述，在此基礎上對通信網絡協(xié)議的形式化方法進行了探究，并給出了一些自己的看法和建議。

【關鍵詞】 通信網絡協(xié)議 形式化方法 協(xié)議要素 描述技術

一、前言

隨著計算機網絡技術的不斷發(fā)展及廣泛應用，新一代的通信網絡逐漸向著數字化、智能化和個人化發(fā)展，網絡所提供的服務也開始由傳統(tǒng)的通信服務逐漸向信息服務轉變。隨著軟件的不斷增多，結構越來越復雜，通信網絡協(xié)議也面臨著越來越多的困難。與此同時，網絡系統(tǒng)在空間分布性、不穩(wěn)定性及多樣性方面表現出來的復雜性對通信網絡協(xié)議的完整性、正確性、可靠性及標準化都提出了更高的要求。伴隨著通信網絡協(xié)議開發(fā)成本的增加，市場競爭的周期開始縮短，在通信網絡協(xié)議的開發(fā)和設計上采用協(xié)議工程技術和方法，并有效實現通信網絡設計合使用過程的規(guī)范化和自動化，成為當前通信網絡協(xié)議開發(fā)課題中的熱點及難點問題。本文就圍繞著通信網絡協(xié)議開發(fā)的形式化方法進行探究。

二、網絡協(xié)議的要素分析

能夠確保計算機網絡順利進行數據通信的通信網絡協(xié)議，其要素主要包括以下幾點：第一，網絡協(xié)議所能提供的服務；第二，網絡協(xié)議運行環(huán)境的假設；第三，實現網絡協(xié)議的詞匯信息及對每個詞匯信息進行的編碼；第四，控制消息保持一致性的規(guī)則。

能夠在計算機之間實現網絡數據通信自動化的協(xié)議，一般來說都是很復雜的，針對這種復雜的問題，采用分層結構來理解網路協(xié)議，具有重要作用。其中，“七層”協(xié)議結構模型是當前網絡協(xié)議中的標準結構，是網絡協(xié)議開發(fā)的基礎。

三、網絡協(xié)議形式化方法、形式化模型及描述

網絡協(xié)議形式化方法是采用數學方法對目標軟件的系統(tǒng)性質進行描述的一種技術方法。通過使用數學符號及數學法則就目標軟件系統(tǒng)的結構來進行綜合分析，研究，為網絡協(xié)議的開發(fā)和驗證提供一個利于發(fā)現目標軟件和系統(tǒng)需求不完整性、不一致性等問題的框架。網絡協(xié)議的形式化方法主要還是通過形式描述技術，即FDT技術來獲得支持，形式化方法描述與模型技術及形式描述語言息息相關。

網絡協(xié)議的形式化模式，其核心技術就是對協(xié)議進行分析和設計。形式化模型主要有以下幾種：第一，有限狀態(tài)機模型。這種模型主要在有限狀態(tài)集、輸入集和轉移規(guī)則集，其中，有限狀態(tài)集一般用于對系統(tǒng)不同狀態(tài)進行描述；輸入集則對系統(tǒng)接受的不同信息進行表征；狀態(tài)轉移規(guī)則集則主要是對表述系統(tǒng)在接受不同輸入時，轉移到下一個狀態(tài)的規(guī)則。第二，Petri網模型，此種模型是適用于并發(fā)、異步及分布式系統(tǒng)描述和分析的數學工具，是目前網絡協(xié)議中的典型模型之一，具有靜態(tài)結構和動態(tài)行為機制。第三，協(xié)議時態(tài)邏輯模型，此種模型在時間信息的事件、狀態(tài)及其關系命題中予以應用，對標識系統(tǒng)中的個體常量、定義變量等進行表達，進而對協(xié)議進行描述。

四、SDL

SDL產生于1976年，是由ITU-T發(fā)展的一種FDT，它是一種基于有限狀態(tài)機建立的數學模型，用于事件驅動、實時和通信系統(tǒng)的描述語言。其形式化方法主要是作為對開發(fā)結果進行驗證、測試的基礎，為設計和應用人員提供交流的途徑，進而為開發(fā)者提供一種分析、設計的方法。SDL著重從全局的視角來對系統(tǒng)結構進行描述，對系統(tǒng)中哪些是由子系統(tǒng)構成，各子系統(tǒng)之間如何相互作用等進行描述，進而遞歸式的對各子系統(tǒng)功能和結構進行描述。

SDL分為圖形和文本兩種形式，對系統(tǒng)功能進行說明，并對系統(tǒng)內部結構行為進行描述。純文本表示更容易被計算機處理；而圖形表示則更直觀，利于進行可視化建模。SDL對一種層次結構來進行描述說明，其結構和功能并明確劃分，功能塊之間通過信道相連；同時，各個功能塊還可以分為子功能塊或進程。SDL對一些基本數據類型和操作以及對構造新的類型進行了定義，因此可以用于系統(tǒng)設計和實現。對SDL的優(yōu)缺點而言，SDL能夠通過全局視角，遞歸式的對各子系統(tǒng)功能及結構進行描述，并對硬件系統(tǒng)和其他各種人造或非人造系統(tǒng)進行描述。與此同時，SDL也具有一定的缺點，例如，SDL不適用于對需要大量進程的緊密協(xié)作，不能對并行處理和應用進行很好的處理；不能適應所有類型的實時系統(tǒng)等。

五、LOTOS

LOTOS產生于1989年，是用于詳細說明和通信系統(tǒng)的描述技術標準形式，適應協(xié)議工程、分布處理及并行處理技術的要求，進而形成的規(guī)范語言，充分引入抽象的數據類型，對進程行為及交互作用進行描述。LOTOS主要是針對分布式的開放系統(tǒng)規(guī)范，尤其對開放式系統(tǒng)連接計算機網絡架構的服務與協(xié)定，進行形式化的技術描述。LOTOS被用來對系統(tǒng)中事件發(fā)生順序來建立運作模式，通過衍生自過程的運作模式和引入抽象數據形態(tài)結構來分析，提供對特定抽象數據形態(tài)的對等描述。LOTOS中的一個系統(tǒng)可以當做多個相互通信的進程；同時，這些進程又可以由多個子進程構成，進行一個規(guī)范的層次結構。一個進程通過門徑和內部行為的時序關系來進行交互和定義；兩個進程通過一個門徑，可以對數值進行匹配，行程三種交互作用，這種進程行為為表達式描述。

六、ESTELLE

ESTELLE開始于1981年，由ISO發(fā)起，在1989年被批準為國際ISO標準，能夠實現完整、一致、簡練的描述分布，并對信息進行處理。ESTELLE使用的是Pascal語法和數據類型，基于擴展的通信有限狀態(tài)機理論，在事件驅動行為建模中進行數據處理方面，能夠準確描述并發(fā)布信息系統(tǒng)，因此，特別適合用于通信協(xié)議。ESTELLE是有許多相互通信的模塊分層構成的系統(tǒng)，在每一級別中可以有多個模塊，同時，每個模塊和子模塊中，都能通過通道以異步方式或凄然模塊進行通信，而通道則是在兩個實體之間相互傳送的結構化雙向路由。其本元素為模塊，由模塊頭和模塊體組成。其中，模塊頭被定義為外部交互點和輸出變量。模塊體則被定義為三個部分，即初始化部分，說明部分和躍遷部分。根據模塊中是否包含狀態(tài)變遷，可以分為三種類型，即活躍模塊。目前，在ESTELLE中，已經開發(fā)看多個用于設計、調試、測試的工具，形成了一套完整的ESTELLE開發(fā)工具套。ESTELLE與SDL的擴展基本一致，但在某些概念上有所不同，ESTELLE擴展主要體現在：用變量和變量型的表示狀態(tài)空間不一樣；所用參數表示交互的方式不一樣；操作與變遷相聯系的方式也不一樣。ESTELLE大部分主要集中在對ISO的應用協(xié)議進行描述。

七、Petri網

Petri網是在1962年，德國的Carl Adam Petri的博士論文中提出，是使用網狀結構模擬通信系統(tǒng)，研究信息系統(tǒng)及其相互關系的數學模型，用于并發(fā)和分布系統(tǒng)行為描述的建模技術，目前，Petri網還沒有明確的國際標準，但已經在分布式系統(tǒng)和通信協(xié)議的相關驗證機性能分析反面得到了廣泛應用。PN是對某一個系統(tǒng)狀態(tài)及變化所提供的圖形表達方式，通過可視描述功能，能夠對模擬系統(tǒng)的動態(tài)和活動行為進行標記。一組通信實體能夠被描述為單一的或相互通信的Petri網模型，由位置和躍遷表示通道實現，網絡的動態(tài)特征，例如控制和數據流等由標記進行分布描述。為了適應不同協(xié)議的需求，Petri模型逐漸擴展到多個模型系統(tǒng)。近年來，Petri網技術得到了極大發(fā)展，各種網系統(tǒng)被開發(fā)，例如，條件/事件網，變遷網，有色網等，這些網絡協(xié)同的開發(fā)對復雜系統(tǒng)的建模能力實現了很大的擴展作用。

Petri網對系統(tǒng)結構能夠較好的描述，對系統(tǒng)中并發(fā)、同步、沖突及順序等關系，可以用圖形等來表示組合模型，更具有直觀、易懂和易用的優(yōu)勢。Petri網具有嚴格定義的數學對象，具備完善的數學理論為基礎。Petri網作為系統(tǒng)建模的工具，在系統(tǒng)設計和分析中，著眼于系統(tǒng)發(fā)生的變化，以及變化發(fā)生的條件和影響。因此，從組織結構的角度來看，其模擬系統(tǒng)不涉及系統(tǒng)所依賴的物理和化學原理；精確描述系統(tǒng)中事件的依賴關系與不依賴關系，這是事件之間的客觀存在，也不依賴與觀察的關系；Petri網還具有與應用環(huán)境無關的動態(tài)行為，作為可獨立的研究對象，且Petri網可以在具有不同應用領域中得到不同的解釋，進而起到溝通不同領域間橋梁的作用和效果。

八、結束語

形式化方法被用于描述復雜的系統(tǒng)，對通信系統(tǒng)的描述、實現和測試均變得十分容易，對此，在通信網絡協(xié)議的開發(fā)設計中，就應該積極采用一些形式化的方法，在網絡協(xié)議開發(fā)和使用效率及降低開發(fā)成本上做出貢獻。

綜上所述，通過對形式化方法在建模、驗證及性能分析方面的比較，在對某些性質或協(xié)議工程的某些階段的工作的秒速比較好，而在其他階段和方面則表現出一些缺陷。例如，SDL在分析技術方面較為缺乏，LOTOS對于所描述的協(xié)議抽象性級別比較高，Petri網則在復雜語義和時序方面進行擴展的描述到具體實現的差距較大。由此可見，通信網絡協(xié)議開發(fā)的形式化方法多有不同，尚沒有一個完全泛用型的方法。因此，在對通信網絡協(xié)議進行開發(fā)時就要在關鍵過程中引入形式化方法。

參考文獻

[1]魯來鳳，吳振強，馬建峰.基于PCL的改進型Helsinki協(xié)議的形式化分析[J].華中科技大學學報（自然科學版），2011（4）：34-36

[2]王惠斌.安全認證協(xié)議的設計與分析[D].解放軍信息工程大學，2010.11：111-113

[3]羅軍舟.從Petri網到形式描述技術和協(xié)議工程.軟件學報，2000，11（5）：606-615

[4]古天龍，蔡國永.網絡協(xié)議的形式化分析與設計.北京：電子工業(yè)出版社， 2003，11（12）：54-57[5]潘紅艷，于全.用于通信網絡協(xié)議開發(fā)的形式化方法[J].計算機工程，2004，30（01）：129-131

[6]徐文超.網絡協(xié)議的形式化分析與設計[J].信息技術，2012，11（02）：121-123