彭 勃

?

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

彭 勃

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

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

計(jì)算機(jī)網(wǎng)絡(luò)；協(xié)議；協(xié)議工程；協(xié)議驗(yàn)證；Petri網(wǎng)

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

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

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

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

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

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

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

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

2 計(jì)算機(jī)網(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é)議比較多，如：高級(jí)數(shù)據(jù)鏈路控制協(xié)議、點(diǎn)到點(diǎn)協(xié)議（PPP）、數(shù)字?jǐn)?shù)據(jù)網(wǎng)（DDN）、綜合業(yè)務(wù)數(shù)字網(wǎng)（ISDN）、數(shù)字用戶線（XDSL）等協(xié)議。

2.3 路由選擇協(xié)議

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

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

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

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

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

5 基于有限狀態(tài)自動(dòng)機(jī)模型的協(xié)議驗(yàn)證與分析

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

6 基于時(shí)序邏輯的協(xié)議描述與驗(yàn)證

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

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

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

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

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

[3]張沖，劉涌，楊海波，等.移動(dòng)社交網(wǎng)絡(luò)實(shí)時(shí)通信機(jī)制的研究[J].計(jì)算機(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