彭 勃

?

計算機網(wǎng)絡(luò)通信協(xié)議驗證技術(shù)的研究

彭 勃

北京聯(lián)海信息系統(tǒng)有限公司，北京 100053

協(xié)議設(shè)計、開發(fā)的復(fù)雜性的增加，導(dǎo)致了協(xié)議工程技術(shù)的出現(xiàn)。針對協(xié)議工程活動中的協(xié)議驗證與分析階段，闡述了驗證技術(shù)的目的與方法，分析了當(dāng)今常用的協(xié)議模型技術(shù)，重點介紹了基于Petri網(wǎng)、FMS，以及時序邏輯TL模型的協(xié)議驗證技術(shù)。

計算機網(wǎng)絡(luò)；協(xié)議；協(xié)議工程；協(xié)議驗證；Petri網(wǎng)

通信協(xié)議（communication protocol）是一組實體在執(zhí)行某項任務(wù)中相互通信行為的規(guī)則和格式（語法和語義）[1]，它是數(shù)據(jù)通訊、計算機網(wǎng)絡(luò)、多機系統(tǒng)等分布式系統(tǒng)的靈魂。隨著網(wǎng)絡(luò)與分布式系統(tǒng)的迅速發(fā)展，通信協(xié)議的形式化技術(shù)，其中包括一系列形式化理論、模型及實現(xiàn)方法已獲得了長足的進步。所謂協(xié)議的形式化技術(shù)是指協(xié)議及服務(wù)規(guī)范的形式描述、設(shè)計驗證、實現(xiàn)驗證和一致性測試。在這些形式化技術(shù)中，形式描述與驗證技術(shù)是整個協(xié)議設(shè)計與實現(xiàn)的基礎(chǔ)，對協(xié)議實現(xiàn)的正確性、完全性和復(fù)雜度有至關(guān)重要的影響。

1 計算機網(wǎng)絡(luò)協(xié)議的定義及特性

1.1 網(wǎng)絡(luò)協(xié)議定義

網(wǎng)絡(luò)協(xié)議是指在計算機與計算機之間進行通信必須遵循的一些事先約定好的規(guī)則。網(wǎng)絡(luò)協(xié)議必須遵循標準化的體系結(jié)構(gòu)，目前主要有ISO的標準和TCP/IP協(xié)議組標準，通信涉及的所有部分必須認同一套用于信息交換的規(guī)則。

1.2 網(wǎng)絡(luò)協(xié)議特性

（1）活動性（liveness）：協(xié)議的活動性體現(xiàn)在終止性和進展性兩方面，或者說，如果協(xié)議有終止性和進展性，它就具有活動性。如果協(xié)議的某個狀態(tài)從初態(tài)不可達，則表明協(xié)議有錯誤。

（2）安全性（Safety）：指協(xié)議運行時錯誤的行動、錯誤的條件等，導(dǎo)致兩種現(xiàn)象發(fā)生：死鎖（deadlock）和活鎖（livelock）。最典型的死鎖是協(xié)議中各實體都處于這樣的一種等待狀態(tài)，即只有在“某一事件”發(fā)生后才做進一步的動作，但在該狀態(tài)下，這個“某一事件”卻不可能發(fā)生。死鎖發(fā)生時，協(xié)議所處的狀態(tài)稱為死鎖狀態(tài)，死鎖的另一種形式是協(xié)議處于無限的死循環(huán)中，而沒有別的事件可使協(xié)議從這一循環(huán)中解脫出來。例如，協(xié)議無限制地執(zhí)行超時重發(fā)操作，但總是收不到對方的確認信息。有人將這種形式的死鎖稱為活鎖，表明整個協(xié)議的狀態(tài)還是變化的，不過不能脫離這種死循環(huán)狀態(tài)而已。

（3）有界性、完整性及可恢復(fù)性或同步性：檢驗協(xié)議的某些成分或參數(shù)的容量（例如通道容量、窗口容量）是否有界。檢驗協(xié)議是否缺少應(yīng)有的處理，以及有無非期待的接收（即錯收）等。這是當(dāng)出現(xiàn)差錯后，協(xié)議能否在有限的步驟內(nèi)返回到正常狀態(tài)（包括初態(tài)）下執(zhí)行。

2 計算機網(wǎng)絡(luò)協(xié)議的分類

2.1 局域網(wǎng)協(xié)議

局域網(wǎng)協(xié)議定義了在多種局域網(wǎng)介質(zhì)上的通信。目前，常用的局域網(wǎng)主要有NetBEUI、IPX/SPX以及其兼容協(xié)議和TCP/IP三類。

2.2 廣域網(wǎng)協(xié)議

廣域網(wǎng)協(xié)議是在OSI參考模型的最下面三層操作。定義了在不同的廣域網(wǎng)介質(zhì)上的通信。主要用于廣域網(wǎng)的通信協(xié)議比較多，如：高級數(shù)據(jù)鏈路控制協(xié)議、點到點協(xié)議（PPP）、數(shù)字數(shù)據(jù)網(wǎng)（DDN）、綜合業(yè)務(wù)數(shù)字網(wǎng)（ISDN）、數(shù)字用戶線（XDSL）等協(xié)議。

2.3 路由選擇協(xié)議

路由選擇協(xié)議是網(wǎng)絡(luò)層協(xié)議，它負責(zé)路徑的選擇和交換。路由選擇協(xié)議還分為內(nèi)部路由協(xié)議（自治系統(tǒng)內(nèi)部交換路由信息的路由協(xié)議）和外部路由協(xié)議（為連接兩個或多個自治系統(tǒng)的路由協(xié)議）。

3 協(xié)議驗證技術(shù)的目的與方法

對協(xié)議本身的邏輯正確性進行校驗的過程稱之為驗證。協(xié)議驗證有兩種途徑：協(xié)議分析和協(xié)議綜合，通常所說的協(xié)議驗證指的是前者。協(xié)議分析的目的是：對已設(shè)計的協(xié)議進行分析和校驗 這些已設(shè)計的協(xié)議大都是采用非形式化設(shè)計（方法產(chǎn)生的）。協(xié)議的正確性驗證試圖在協(xié)議開發(fā)的前期最大限度地檢測和糾正協(xié)議錯誤和缺陷，包括死鎖、活鎖、不可執(zhí)行的行動、協(xié)議外部性能不符合服務(wù)要求等。協(xié)議驗證技術(shù)多種多樣但可以分為3類：可達性分析是最常用的技術(shù)，它包括狀態(tài)窮舉、狀態(tài)隨機枚舉、狀態(tài)概率枚舉等方法；邏輯證明試圖用推理演算方法嚴密的證明協(xié)議各種性質(zhì)，采用的推理演算技術(shù)主要來自與時序邏輯、謂詞邏輯、代數(shù)演算等數(shù)學(xué)領(lǐng)域；第三類驗證技術(shù)是模擬。協(xié)議綜合將協(xié)議設(shè)計和協(xié)議驗證緊密結(jié)合起來，也可以認為是一類驗證技術(shù)。

4 網(wǎng)絡(luò)協(xié)議中Ping程序及其應(yīng)用

這個程序用來檢測一幀數(shù)據(jù)從當(dāng)前主機傳送到目的主機所需要的時間。當(dāng)網(wǎng)絡(luò)運行中出現(xiàn)故障時，采用這個實用程序來預(yù)測故障和確定故障源是非常有效的。如果執(zhí)行ping不成功，則可以預(yù)測故障出現(xiàn)在以下幾個方面：網(wǎng)線是否連通，網(wǎng)絡(luò)適配器是否正確，IP地址是否可用等；如果執(zhí)行ping成功而網(wǎng)絡(luò)仍然不能使用，那么問題很可能出現(xiàn)在網(wǎng)絡(luò)系統(tǒng)的軟件配置方面，ping成功只能保證當(dāng)前主機與目的主機存在一條連通的物理路徑，它還提供了許多參數(shù)，如-t使用當(dāng)前主機不斷向目的主機發(fā)送數(shù)據(jù)，直到使用ctel-c中斷；-n可以自己確定想目的主機發(fā)送數(shù)據(jù)偵數(shù)等等。

5 基于有限狀態(tài)自動機模型的協(xié)議驗證與分析

有限狀態(tài)機FSM是最為重要的一種形式描述技術(shù)，它是很多形式化方法的基礎(chǔ)。它直觀性強，可實現(xiàn)與其他形式方法的組合和轉(zhuǎn)換，且易于自動實現(xiàn)[2]，因而在FDT中占有重要的地位。有限狀態(tài)機最常用的技術(shù)是可達性分析技術(shù)?？蛇_性分析技術(shù)試圖產(chǎn)生和檢查協(xié)議所有或部分可達狀態(tài)。一般來說，對于每次發(fā)生的轉(zhuǎn)變，可通過使用系統(tǒng)全局狀態(tài)來決定特性，像是否表示一個死鎖狀態(tài)，所有實體是否在當(dāng)前狀態(tài)能接收發(fā)給它的所有報文等?；贔SM描述的協(xié)議驗證可通過構(gòu)造可達樹來實現(xiàn)?？蛇_樹的根為系統(tǒng)的初始狀態(tài)[3]。從初始狀態(tài)出發(fā)，列舉出全部可能的轉(zhuǎn)移，每一個轉(zhuǎn)移將產(chǎn)生一個新的狀態(tài)空間。在此葉結(jié)點的基礎(chǔ)上，不斷生長新的葉節(jié)點，直到?jīng)]有新的葉節(jié)點為止?？蛇_樹上各節(jié)點分別表示某一給定時刻的全局狀態(tài)矩陣（GMS），它動態(tài)地反映了兩個或多個協(xié)議實體或進程的交互活動。FSM由于簡單、直觀而得到廣泛應(yīng)用，但不利于協(xié)議驗證的實現(xiàn)，不易于描述復(fù)雜的系統(tǒng)。

6 基于時序邏輯的協(xié)議描述與驗證

從邏輯角度來說，時序邏輯TL（Tempoeal Longic）是模態(tài)邏輯的擴充，以狀態(tài)為可能世界，以狀態(tài)的演變次序關(guān)系為可能世界間的可到達關(guān)系。時序邏輯的種類很多，隨時間結(jié)構(gòu)不同，算子的選擇也有差異。時序邏輯應(yīng)用較為成熟，并且數(shù)學(xué)抽象能力很強，它側(cè)重于通過定義系統(tǒng)外部可見的行為事件來描述系統(tǒng)，即直接描述系統(tǒng)的輸入/輸出行為，而不關(guān)心協(xié)議實體的內(nèi)部變化，比FSM、Petri網(wǎng)更易于刻劃協(xié)議的活動性，因而有利于對協(xié)議的各種性質(zhì)進行分析驗證。

7 其他協(xié)議分析技術(shù)

除前面介紹的協(xié)議形式化技術(shù)以外，由R.Miler開拓性創(chuàng)建的通訊進程演算CCS（the SCalcula for Communicating System），以及C.A.R.Hoare在基礎(chǔ)上創(chuàng)立的通訊順序進程CSP（the Communing Sequential processes）也在協(xié)議工程中得到了重要的應(yīng)用。

[1]張小亮，涂勇策，馬恒太，等.一種適用于衛(wèi)星通信網(wǎng)絡(luò)的端到端認證協(xié)議[J].計算機研究與發(fā)展，2013，50（3）：540-547.

[2]朱雪寒，夏卓群，劉品超，等.基于網(wǎng)絡(luò)編碼的ECC驗證方案在WSN中的研究[J].計算機技術(shù)與發(fā)展，2011，21（2）：173-176.

[3]張沖，劉涌，楊海波，等.移動社交網(wǎng)絡(luò)實時通信機制的研究[J].計算機系統(tǒng)應(yīng)用，2014，23（2）：205-208.

Computer Network Communication Protocol Verification Technology

Peng Bo

Beijing MINUSTAH Information System Co., Ltd.,Beijing 100053

Protocol design，complexity increases development，led to the emergence of protocol engineering technologies for protocol engineering activities protocol verification and analysis phases，on the purposes and methods of verification technology， analyzes commonly used today protocol model technology，focusing on the verification protocol based on Petri nets，F(xiàn)MS，and temporal logic TL model technology.

computer network；protocol engineering；protocol validation；Petri nets

TP393.04

A

1009-6434(2016)07-0108-02