用于通信網(wǎng)絡(luò)協(xié)議開發(fā)的形式化方法

李新宇

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

【關(guān)鍵詞】 通信網(wǎng)絡(luò)協(xié)議 形式化方法 協(xié)議要素 描述技術(shù)

一、前言

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

二、網(wǎng)絡(luò)協(xié)議的要素分析

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

能夠在計(jì)算機(jī)之間實(shí)現(xiàn)網(wǎng)絡(luò)數(shù)據(jù)通信自動(dòng)化的協(xié)議，一般來說都是很復(fù)雜的，針對(duì)這種復(fù)雜的問題，采用分層結(jié)構(gòu)來理解網(wǎng)路協(xié)議，具有重要作用。其中，“七層”協(xié)議結(jié)構(gòu)模型是當(dāng)前網(wǎng)絡(luò)協(xié)議中的標(biāo)準(zhǔn)結(jié)構(gòu)，是網(wǎng)絡(luò)協(xié)議開發(fā)的基礎(chǔ)。

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

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

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

四、SDL

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

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

五、LOTOS

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

六、ESTELLE

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

七、Petri網(wǎng)

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

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

八、結(jié)束語

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

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

參考文獻(xiàn)

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

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

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

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

[6]徐文超.網(wǎng)絡(luò)協(xié)議的形式化分析與設(shè)計(jì)[J].信息技術(shù)，2012，11（02）：121-123