網(wǎng)絡(luò)協(xié)議的形式化分析與設(shè)計(jì)

徐文超

摘 要：隨著形式化方法和技術(shù)的日趨完善，網(wǎng)絡(luò)協(xié)議的開(kāi)發(fā)已逐步從非形式化描述、手工方法實(shí)現(xiàn)過(guò)渡到已形式化描述技術(shù)為基礎(chǔ)，滲透到網(wǎng)絡(luò)協(xié)議分析、綜合、測(cè)試等各環(huán)節(jié)的軟件工程方法。本文從網(wǎng)絡(luò)協(xié)議的基本要素、協(xié)議的形式化模型介紹了網(wǎng)絡(luò)協(xié)議，并從協(xié)議的性質(zhì)描述、不變性分析、可達(dá)性分析、基于有序二叉判決圖的符號(hào)模型檢驗(yàn)對(duì)網(wǎng)絡(luò)協(xié)議進(jìn)行了形式化設(shè)計(jì)與驗(yàn)證，最后進(jìn)行了測(cè)試。

關(guān)鍵詞：網(wǎng)絡(luò)協(xié)議 形式化分析 符號(hào)模型檢驗(yàn)

中圖分類號(hào)：T298K2 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：1672-3791（2013）（03）（b）-0034-02

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

1 網(wǎng)絡(luò)協(xié)議的基本要素

一套完整的，能夠確保計(jì)算機(jī)網(wǎng)絡(luò)可以順利進(jìn)行數(shù)據(jù)通信的網(wǎng)絡(luò)協(xié)議要包括下邊的五點(diǎn)基本要素：（1）協(xié)議所提供的服務(wù)。（2）對(duì)協(xié)議運(yùn)行環(huán)境所進(jìn)行的假設(shè)。（3）用來(lái)實(shí)現(xiàn)協(xié)議的消息詞匯。（4）對(duì)該詞匯中每個(gè)消息的編碼。（5）用來(lái)控制消息一致性的過(guò)程規(guī)則。

實(shí)現(xiàn)計(jì)算機(jī)之間高度自動(dòng)化數(shù)據(jù)通信的網(wǎng)絡(luò)協(xié)議，一般都會(huì)極其復(fù)雜。借鑒對(duì)復(fù)雜系統(tǒng)問(wèn)題分析研究的思想，分層結(jié)構(gòu)對(duì)于理解和設(shè)計(jì)網(wǎng)絡(luò)協(xié)議有著重要的作用?！捌邔印眳f(xié)議結(jié)構(gòu)模型是目前網(wǎng)絡(luò)協(xié)議的標(biāo)準(zhǔn)體系結(jié)構(gòu)，也成為了網(wǎng)絡(luò)協(xié)議開(kāi)發(fā)的基礎(chǔ)。

2 協(xié)議的形式化模型

協(xié)議分析和設(shè)計(jì)其中一項(xiàng)核心技術(shù)就是形式化模型。網(wǎng)絡(luò)協(xié)議的形式化規(guī)格可以在形式化模型的基礎(chǔ)上實(shí)現(xiàn)，從而為協(xié)議的形式化分析與驗(yàn)證、協(xié)議綜合、協(xié)議測(cè)試、以及協(xié)議實(shí)現(xiàn)等提供良好的基礎(chǔ)。形式化模型包括以下幾點(diǎn)。

2.1 協(xié)議的有限狀態(tài)機(jī)模型

有限狀態(tài)機(jī)包括有限狀態(tài)集、輸入集和狀態(tài)轉(zhuǎn)移規(guī)則集；有限狀態(tài)集，用于描述系統(tǒng)中的不同狀態(tài)；輸入集用于表征系統(tǒng)所接收的不同輸入信息；狀態(tài)轉(zhuǎn)移規(guī)則集用于表述系統(tǒng)在接收不同輸入下從一個(gè)狀態(tài)轉(zhuǎn)移到另外一個(gè)狀態(tài)的規(guī)則。

2.2 Petri網(wǎng)模型

Petri網(wǎng)是一種適合于并發(fā)、異步、分布式系統(tǒng)描述與分析的圖形數(shù)學(xué)工具。Petri網(wǎng)已成為網(wǎng)絡(luò)協(xié)議分析和設(shè)計(jì)的典型形式模型之一。它作為系統(tǒng)描述和分析的工具，除了具有靜態(tài)結(jié)構(gòu)外，還包括了描述系統(tǒng)動(dòng)態(tài)行為的機(jī)制。這一特征是通過(guò)允許位置中包含令牌，令牌可以依據(jù)遷移的引發(fā)而重新分布來(lái)實(shí)現(xiàn)的。

2.3 協(xié)議的時(shí)態(tài)邏輯模型

時(shí)態(tài)邏輯是模態(tài)邏輯的擴(kuò)充，它涉及含有時(shí)間信息的事件、狀態(tài)及其關(guān)系的命題、謂詞和演算。要描述一個(gè)協(xié)議，首先要標(biāo)識(shí)系統(tǒng)中的個(gè)體常量，定義變量，表達(dá)命題、謂詞函數(shù)。以下為命題與謂詞的表達(dá)。

（1）個(gè)體常量m0，m1表示序號(hào)為0，1的報(bào)文；any表示無(wú)序號(hào)的任意報(bào)文；ack0，ack1表示序號(hào)為0，1的認(rèn)可報(bào)文。

（2）個(gè)體變量m代表m0，m1，any；ack代表ack0，ack1；seq代表0，1序號(hào)；a代表原子行動(dòng)或事件。

（3）謂詞at（a）開(kāi)始一個(gè)協(xié)議行動(dòng)或事件。

2.4 通信進(jìn)程演算模型

通信進(jìn)程演算是計(jì)算機(jī)通信系統(tǒng)的基本理論模型，它也是許多形式化語(yǔ)言的基礎(chǔ)。通信進(jìn)程演算的基本成分是事件與進(jìn)程，而進(jìn)程是通過(guò)順序、選擇和并行三個(gè)基本算子來(lái)定義的。一般用大寫(xiě)字母來(lái)表示進(jìn)程，用小寫(xiě)字母來(lái)表示事件。

3 協(xié)議的形式化設(shè)計(jì)與驗(yàn)證

協(xié)議的設(shè)計(jì)驗(yàn)證是對(duì)協(xié)議的功能和性能進(jìn)行校驗(yàn)的過(guò)程，是保證協(xié)議開(kāi)發(fā)質(zhì)量的必要環(huán)節(jié)。協(xié)議形式化驗(yàn)證首先需要對(duì)協(xié)議性質(zhì)進(jìn)行系統(tǒng)的語(yǔ)言描述，然后基于協(xié)議的形式模型或者形式語(yǔ)言進(jìn)行描述，通過(guò)適當(dāng)?shù)募夹g(shù)對(duì)協(xié)議性質(zhì)進(jìn)行分析校驗(yàn)。

3.1 協(xié)議的性質(zhì)描述

設(shè)計(jì)網(wǎng)絡(luò)協(xié)議的目的就是設(shè)計(jì)出的協(xié)議要滿足功能和性能。一方面，協(xié)議本身應(yīng)用問(wèn)題的特征性對(duì)協(xié)議的功能和性能具有特殊的要求；另外一方面，協(xié)議的功能和性能所擁有的協(xié)議的性質(zhì)，是獨(dú)立于問(wèn)題的一般性要求。協(xié)議的性質(zhì)包括活性、安全性、一致性、完備性、可恢復(fù)性和有界性六方面。

（1）活性就是指無(wú)死鎖性，如果在協(xié)議運(yùn)行時(shí)候發(fā)生一些好事，就叫協(xié)議的活性，像發(fā)生預(yù)定的事情，能夠到達(dá)指定的協(xié)議狀態(tài)，可以進(jìn)行應(yīng)該進(jìn)行的協(xié)議活動(dòng)等都是協(xié)議的好事情。協(xié)議的終止性和進(jìn)展性兩反面可以體現(xiàn)協(xié)議的活性。也就是說(shuō)具有終止性和進(jìn)展性的協(xié)議就擁有活性。如果協(xié)議能夠在從任何一狀態(tài)下開(kāi)始運(yùn)行都能正確的到達(dá)終止?fàn)顟B(tài)，就是協(xié)議的終止性。終止?fàn)顟B(tài)在某些情況下也會(huì)和初始狀態(tài)是同一個(gè)。所以協(xié)議總能從初始狀態(tài)開(kāi)始運(yùn)行然后正確的回到初始狀態(tài)，并可反復(fù)運(yùn)行，這就是協(xié)議的可重復(fù)性，即可重復(fù)性=終止性+進(jìn)展性=活動(dòng)性。

（2）安全性就是沒(méi)有壞的事情出現(xiàn)在協(xié)議運(yùn)行的時(shí)候。像不可接收事件、不可進(jìn)一步向前的狀態(tài)、錯(cuò)誤的行動(dòng)、錯(cuò)誤的條件、變量值越界等都是壞的事情。壞事情一般會(huì)導(dǎo)致死鎖和活鎖兩種情況發(fā)生。

（3）一致性就是指協(xié)議的服務(wù)行為和協(xié)議行為保持一致。像協(xié)議需要為用戶提供的所要求的業(yè)務(wù)和不用提供用戶沒(méi)有要求提供的業(yè)務(wù)都體現(xiàn)了協(xié)議的一致性。

（4）完備性，協(xié)議擁有完全符合協(xié)議環(huán)境各種要求的性質(zhì)，也就是在考慮了用戶要求、用戶特點(diǎn)、通道性質(zhì)、工作模式等各種潛在影響因素之后構(gòu)建的協(xié)議構(gòu)造，同時(shí)兼?zhèn)淇紤]各種錯(cuò)誤事件以及異常情況的處理。

（5）可恢復(fù)性是指當(dāng)協(xié)議出現(xiàn)差錯(cuò)后，協(xié)議本身能否在有限的步驟內(nèi)返回到正常狀態(tài)下執(zhí)行?？苫謴?fù)性是和可重復(fù)性相關(guān)聯(lián)的一個(gè)性質(zhì)。

（6）有界性是與協(xié)議中的變量和參數(shù)有關(guān)的一個(gè)性質(zhì)，用來(lái)衡量協(xié)議中的變量和參數(shù)是否超過(guò)其限定值。

3.2 不變性分析

系統(tǒng)不變性是某一邏輯公式表達(dá)的系統(tǒng)性質(zhì)的永真性，它不隨系統(tǒng)的狀態(tài)變化或執(zhí)行序列而改變。系統(tǒng)不變性分析實(shí)際包含兩個(gè)任務(wù)。第一是分析系統(tǒng)應(yīng)該具有的不變性質(zhì)，并用邏輯公式來(lái)表示，第二個(gè)任務(wù)是分析系統(tǒng)的執(zhí)行，證明該邏輯公式成立。

3.3 可達(dá)性分析

可達(dá)性分析是試圖產(chǎn)生和檢查協(xié)議所有部分的可達(dá)狀態(tài)，進(jìn)而檢驗(yàn)基于狀態(tài)或者基于狀態(tài)序列的協(xié)議性質(zhì)。所謂可達(dá)狀態(tài)是指協(xié)議從初始狀態(tài)開(kāi)始經(jīng)歷有限次轉(zhuǎn)換之后可達(dá)到的狀態(tài)，所有可達(dá)狀態(tài)構(gòu)成了系統(tǒng)狀態(tài)空間。可達(dá)性分析算法是用來(lái)生成并檢驗(yàn)一個(gè)特定的初始狀態(tài)可達(dá)的所有狀態(tài)算法。

3.4 基于有序二叉判決圖的符號(hào)模型檢驗(yàn)

符號(hào)模型檢驗(yàn)是采用緊湊的信息壓縮形式來(lái)隱式表示系統(tǒng)可達(dá)狀態(tài)和要求證明性質(zhì)的邏輯公式的模型檢驗(yàn)。有序二叉判決圖是隱式、高效率表示狀態(tài)空間的一種數(shù)據(jù)結(jié)構(gòu)?；谟行蚨媾袥Q圖的符號(hào)模型檢驗(yàn)是分析驗(yàn)證協(xié)議系統(tǒng)的有效技術(shù)。

基于有序二叉判決圖實(shí)現(xiàn)的模型檢驗(yàn)算法能有效地避免狀態(tài)爆炸的問(wèn)題，使得驗(yàn)證系統(tǒng)適用的系統(tǒng)規(guī)模擴(kuò)大，現(xiàn)已能對(duì)具有多達(dá)1020個(gè)狀態(tài)的系統(tǒng)進(jìn)行驗(yàn)證?；谟行蚨媾袥Q圖的符號(hào)模型驗(yàn)證主要考慮以下幾個(gè)方面：狀態(tài)的布爾公式表示；狀態(tài)轉(zhuǎn)移關(guān)系的布爾公式表示；Kripke結(jié)構(gòu)的布爾公式表示；CTL公式在布爾公式表示的Kripke結(jié)構(gòu)上的解釋。

現(xiàn)用QBF公式表示Kripke結(jié)構(gòu)，并把用這些符號(hào)表示的Kripke結(jié)構(gòu)上的CTL算子用QBF上的算子來(lái)描述。實(shí)際上，因?yàn)檫壿嬤B接詞在CTL*和QBF上有著相同的意義，所以只需要刻畫(huà)算子EN，而其它的CTL*的算子可以通過(guò)EN和邏輯運(yùn)算的函數(shù)不動(dòng)點(diǎn)進(jìn)行描述。

4 網(wǎng)絡(luò)協(xié)議的測(cè)試

測(cè)試是保證網(wǎng)絡(luò)協(xié)議質(zhì)量的一個(gè)重要手段，是協(xié)議實(shí)現(xiàn)過(guò)程中的一種實(shí)驗(yàn)活動(dòng)。盡管測(cè)試并不能完全證明協(xié)議實(shí)現(xiàn)的正確性，但是在系統(tǒng)的測(cè)試活動(dòng)檢查下，可以把協(xié)議在實(shí)現(xiàn)過(guò)程中出錯(cuò)的概率降低到實(shí)際應(yīng)用可以接受的程度。

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

5 結(jié)語(yǔ)

形式化方法是基于嚴(yán)密的、數(shù)學(xué)上的形式機(jī)制的系統(tǒng)研究方法?？陀^地講，有了數(shù)學(xué)的應(yīng)用，就有了形式化的方法。迄今為止，形式化方法成功地應(yīng)用于空中交通管制系統(tǒng)、鐵路信號(hào)系統(tǒng)、核電站控制系統(tǒng)、通信系統(tǒng)、醫(yī)療監(jiān)護(hù)系統(tǒng)、硬件電路等諸多領(lǐng)域。網(wǎng)絡(luò)協(xié)議的形式化分析和設(shè)計(jì)正在向完善化、系統(tǒng)化、自動(dòng)化和標(biāo)準(zhǔn)化方向發(fā)展。

參考文獻(xiàn)

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

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