網絡協議的形式化分析與設計

徐文超

摘 要：隨著形式化方法和技術的日趨完善，網絡協議的開發已逐步從非形式化描述、手工方法實現過渡到已形式化描述技術為基礎，滲透到網絡協議分析、綜合、測試等各環節的軟件工程方法。本文從網絡協議的基本要素、協議的形式化模型介紹了網絡協議，并從協議的性質描述、不變性分析、可達性分析、基于有序二叉判決圖的符號模型檢驗對網絡協議進行了形式化設計與驗證，最后進行了測試。

關鍵詞：網絡協議 形式化分析 符號模型檢驗

中圖分類號：T298K2 文獻標識碼：A 文章編號：1672-3791（2013）（03）（b）-0034-02

協議一詞最早出現在通信系統，協議歷史擁有像通信一樣古老的歷史。從古至今，人們一直都在不斷的探索研究，怎樣才能建立一個能夠在快速在遠距離上傳輸信息的系統。如果想要實現信息在遠距離間傳遞，不光需要硬件設備，也就是發送和接收信號的設備，還需要建立一整套能夠規定信號所代表的意義以及傳遞接收信號方式的規則、標準或者約定，這個規則就是協議。

1 網絡協議的基本要素

一套完整的，能夠確保計算機網絡可以順利進行數據通信的網絡協議要包括下邊的五點基本要素：（1）協議所提供的服務。（2）對協議運行環境所進行的假設。（3）用來實現協議的消息詞匯。（4）對該詞匯中每個消息的編碼。（5）用來控制消息一致性的過程規則。

實現計算機之間高度自動化數據通信的網絡協議，一般都會極其復雜。借鑒對復雜系統問題分析研究的思想，分層結構對于理解和設計網絡協議有著重要的作用。“七層”協議結構模型是目前網絡協議的標準體系結構，也成為了網絡協議開發的基礎。

2 協議的形式化模型

協議分析和設計其中一項核心技術就是形式化模型。網絡協議的形式化規格可以在形式化模型的基礎上實現，從而為協議的形式化分析與驗證、協議綜合、協議測試、以及協議實現等提供良好的基礎。形式化模型包括以下幾點。

2.1 協議的有限狀態機模型

有限狀態機包括有限狀態集、輸入集和狀態轉移規則集；有限狀態集，用于描述系統中的不同狀態；輸入集用于表征系統所接收的不同輸入信息；狀態轉移規則集用于表述系統在接收不同輸入下從一個狀態轉移到另外一個狀態的規則。

2.2 Petri網模型

Petri網是一種適合于并發、異步、分布式系統描述與分析的圖形數學工具。Petri網已成為網絡協議分析和設計的典型形式模型之一。它作為系統描述和分析的工具，除了具有靜態結構外，還包括了描述系統動態行為的機制。這一特征是通過允許位置中包含令牌，令牌可以依據遷移的引發而重新分布來實現的。

2.3 協議的時態邏輯模型

時態邏輯是模態邏輯的擴充，它涉及含有時間信息的事件、狀態及其關系的命題、謂詞和演算。要描述一個協議，首先要標識系統中的個體常量，定義變量，表達命題、謂詞函數。以下為命題與謂詞的表達。

（1）個體常量m0，m1表示序號為0，1的報文；any表示無序號的任意報文；ack0，ack1表示序號為0，1的認可報文。

（2）個體變量m代表m0，m1，any；ack代表ack0，ack1；seq代表0，1序號；a代表原子行動或事件。

（3）謂詞at（a）開始一個協議行動或事件。

2.4 通信進程演算模型

通信進程演算是計算機通信系統的基本理論模型，它也是許多形式化語言的基礎。通信進程演算的基本成分是事件與進程，而進程是通過順序、選擇和并行三個基本算子來定義的。一般用大寫字母來表示進程，用小寫字母來表示事件。

3 協議的形式化設計與驗證

協議的設計驗證是對協議的功能和性能進行校驗的過程，是保證協議開發質量的必要環節。協議形式化驗證首先需要對協議性質進行系統的語言描述，然后基于協議的形式模型或者形式語言進行描述，通過適當的技術對協議性質進行分析校驗。

3.1 協議的性質描述

設計網絡協議的目的就是設計出的協議要滿足功能和性能。一方面，協議本身應用問題的特征性對協議的功能和性能具有特殊的要求；另外一方面，協議的功能和性能所擁有的協議的性質，是獨立于問題的一般性要求。協議的性質包括活性、安全性、一致性、完備性、可恢復性和有界性六方面。

（1）活性就是指無死鎖性，如果在協議運行時候發生一些好事，就叫協議的活性，像發生預定的事情，能夠到達指定的協議狀態，可以進行應該進行的協議活動等都是協議的好事情。協議的終止性和進展性兩反面可以體現協議的活性。也就是說具有終止性和進展性的協議就擁有活性。如果協議能夠在從任何一狀態下開始運行都能正確的到達終止狀態，就是協議的終止性。終止狀態在某些情況下也會和初始狀態是同一個。所以協議總能從初始狀態開始運行然后正確的回到初始狀態，并可反復運行，這就是協議的可重復性，即可重復性=終止性+進展性=活動性。

（2）安全性就是沒有壞的事情出現在協議運行的時候。像不可接收事件、不可進一步向前的狀態、錯誤的行動、錯誤的條件、變量值越界等都是壞的事情。壞事情一般會導致死鎖和活鎖兩種情況發生。

（3）一致性就是指協議的服務行為和協議行為保持一致。像協議需要為用戶提供的所要求的業務和不用提供用戶沒有要求提供的業務都體現了協議的一致性。

（4）完備性，協議擁有完全符合協議環境各種要求的性質，也就是在考慮了用戶要求、用戶特點、通道性質、工作模式等各種潛在影響因素之后構建的協議構造，同時兼備考慮各種錯誤事件以及異常情況的處理。

（5）可恢復性是指當協議出現差錯后，協議本身能否在有限的步驟內返回到正常狀態下執行。可恢復性是和可重復性相關聯的一個性質。

（6）有界性是與協議中的變量和參數有關的一個性質，用來衡量協議中的變量和參數是否超過其限定值。

3.2 不變性分析

系統不變性是某一邏輯公式表達的系統性質的永真性，它不隨系統的狀態變化或執行序列而改變。系統不變性分析實際包含兩個任務。第一是分析系統應該具有的不變性質，并用邏輯公式來表示，第二個任務是分析系統的執行，證明該邏輯公式成立。

3.3 可達性分析

可達性分析是試圖產生和檢查協議所有部分的可達狀態，進而檢驗基于狀態或者基于狀態序列的協議性質。所謂可達狀態是指協議從初始狀態開始經歷有限次轉換之后可達到的狀態，所有可達狀態構成了系統狀態空間。可達性分析算法是用來生成并檢驗一個特定的初始狀態可達的所有狀態算法。

3.4 基于有序二叉判決圖的符號模型檢驗

符號模型檢驗是采用緊湊的信息壓縮形式來隱式表示系統可達狀態和要求證明性質的邏輯公式的模型檢驗。有序二叉判決圖是隱式、高效率表示狀態空間的一種數據結構。基于有序二叉判決圖的符號模型檢驗是分析驗證協議系統的有效技術。

基于有序二叉判決圖實現的模型檢驗算法能有效地避免狀態爆炸的問題，使得驗證系統適用的系統規模擴大，現已能對具有多達1020個狀態的系統進行驗證。基于有序二叉判決圖的符號模型驗證主要考慮以下幾個方面：狀態的布爾公式表示；狀態轉移關系的布爾公式表示；Kripke結構的布爾公式表示；CTL公式在布爾公式表示的Kripke結構上的解釋。

現用QBF公式表示Kripke結構，并把用這些符號表示的Kripke結構上的CTL算子用QBF上的算子來描述。實際上，因為邏輯連接詞在CTL*和QBF上有著相同的意義，所以只需要刻畫算子EN，而其它的CTL*的算子可以通過EN和邏輯運算的函數不動點進行描述。

4 網絡協議的測試

測試是保證網絡協議質量的一個重要手段，是協議實現過程中的一種實驗活動。盡管測試并不能完全證明協議實現的正確性，但是在系統的測試活動檢查下，可以把協議在實現過程中出錯的概率降低到實際應用可以接受的程度。

相對而言，基于有限狀態機模型的協議測試方法有比較高的錯誤覆蓋率。然而，在實際中，協議規格的狀態機模型并不滿足對有限狀態機的假設，即便滿足，相應的測試生成算法也太復雜，生成的測試序列也太長，測試成本太高。隨時著各種各樣的有限狀態機規格的廣泛使用，借助于軟件數據流測試的思想，基于數據流的協議測試序列生成方法相應得到了研究應用。數據流測試通常基于有向數據流圖。在理想情況下，測試所有可能的輸入數據將提供最完全的程序行為信息，而在實際測試中，通常選擇一個可以代表整個輸入域的子集。

5 結語

形式化方法是基于嚴密的、數學上的形式機制的系統研究方法。客觀地講，有了數學的應用，就有了形式化的方法。迄今為止，形式化方法成功地應用于空中交通管制系統、鐵路信號系統、核電站控制系統、通信系統、醫療監護系統、硬件電路等諸多領域。網絡協議的形式化分析和設計正在向完善化、系統化、自動化和標準化方向發展。

參考文獻

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

[2] 王惠斌.安全認證協議的設計與分析[D].解放軍信息工程大學，2010.