基于SPIN的協(xié)議分析驗證研究

摘要:為了研究協(xié)議分析驗證方法的有效性，論文利用協(xié)議分析驗證工具SPIN對可靠傳輸協(xié)議中的GBN協(xié)議進(jìn)行了分析驗證，結(jié)果發(fā)現(xiàn)單純依靠工具并不能保證協(xié)議的正確性，本文對如何確保協(xié)議的正確性進(jìn)行了研究，提出了具體建議。

關(guān)鍵詞:SPIN;協(xié)議分析驗證;Promela語言;GBN協(xié)議

中圖分類號:TP393.08

The research of protocol analysis and verification based on SPIN

HOU Fenghan1 BAI Xiaochong2

(1 Department of Computer Engineering ， Henan Polytechnic Institute， Nanyang， Henan， China， 473009

2 PLA Uint 95865， Changping， Beijing， China， 102218)

Abstract:In order to research the effectivity of the protocol analysis verification， this paper analyzed and verified the reliable transport protocol GBN by protocol analysis tool SPIN. This paper found that only relying on SPIN can not guarantee the correctness of the protocol， studied how to ensure the correctness of the protocol， and made specific recommendations.

Keywords:SPIN; Protocol Analysis and Verification; Promela; GBN

0 引言

計算機(jī)網(wǎng)絡(luò)及數(shù)據(jù)通信是當(dāng)今信息社會的基石，網(wǎng)絡(luò)協(xié)議則是其中不可缺少的重要組成部分，形式化方法與技術(shù)已經(jīng)滲透到網(wǎng)絡(luò)協(xié)議開發(fā)的整個過程[1]。研究人員已開發(fā)出了支持協(xié)議開發(fā)活動中形式化描述、正確性驗證、性能分析、自動代碼生成和一致性測試等各個方面的多種軟件工具，SPIN正是其中進(jìn)行協(xié)議分析驗證的工具。本文利用用協(xié)議分析工具SPIN對可靠傳輸協(xié)議中的GBN協(xié)議進(jìn)行了分析驗證。通過研究，發(fā)現(xiàn)單純依靠工具并不能保證協(xié)議的正確性，論文對如何確保協(xié)議的正確性提出了具體建議。

論文的第1節(jié)簡單介紹協(xié)議分析驗證工具SPIN和形式化描述語言Promela。第2節(jié)簡單介紹GBN協(xié)議及其驗證。第3節(jié)提出單純依靠工具產(chǎn)生的問題及如何確保協(xié)議正確性的具體建議。最后，我們在第4節(jié)對全文進(jìn)行總結(jié)。

1 SPIN及相關(guān)概念

1.1 協(xié)議分析驗證工具SPIN

當(dāng)前，在模型檢驗分析方面人們已經(jīng)開發(fā)出了多種自動化工具，SPIN就是其中比較典型的一種。SPIN的全稱是Simple Promela Interpreter(簡單Promela解釋器)。它是適合于并行系統(tǒng)，尤其是協(xié)議一致性的輔助分析驗證工具。該工具由貝爾實驗室的形式化方法與驗證小組于1980年開始開發(fā)[1]。SPIN軟件是用ANSI C開發(fā)的，可以在Unix操作系統(tǒng)上使用，在windows操作系統(tǒng)上使用則需要安裝不同版本，windows下已經(jīng)開發(fā)出了一個圖形界面的版本XSPIN，本文即使用XSPIN。

1.2 形式化描述語言Promela

Promela語言是SPIN的核心，它的全稱是Protocol/Process Meta Language，是1983年設(shè)計的Argos語言的一個擴(kuò)展，是一種用于描述通信協(xié)議或其他類似的分布式系統(tǒng)的一種抽象語言[2]。Promela類似于C語言，對有限狀態(tài)系統(tǒng)進(jìn)行建模，允許動態(tài)創(chuàng)建并行的進(jìn)程，并可以在進(jìn)程之間通過消息通道進(jìn)行同步(使用會面點(rendezvous port))或異步(使用緩沖)進(jìn)行通信[1]。一個Promela程序由一組相互之間進(jìn)行通信的進(jìn)程構(gòu)成。每一個進(jìn)程是一個擴(kuò)展的有限狀態(tài)機(jī)(EFSM，Extened Finite State Machine)。在這種語言中只支持簡單的數(shù)據(jù)類型，如各種范圍的整形、記錄類型(與C語言中的typedef類似)。

2 GBN協(xié)議及其驗證

2.1 GBN協(xié)議

GBN(Go-Back-N)協(xié)議通常被稱為滑動窗口協(xié)議(sliding-window protocol)，該協(xié)議允許發(fā)送方發(fā)送多個分組(當(dāng)有多個分組時)而不需要等待確認(rèn)，但其受限于管道中未被確認(rèn)的分組數(shù)，此數(shù)目最大不能超過最大允許數(shù)目N，N即為窗口大小。如下圖所示[3]。

2.2 GBN協(xié)議分析驗證

GBN協(xié)議的發(fā)送方響應(yīng)三種事件:

(1)上層調(diào)用:上層調(diào)用udt_send()時，發(fā)送方先檢查發(fā)送窗口是否已滿。如果未滿，則創(chuàng)建一個分組并發(fā)送，否則上層將等待一段時間再試。

(2)ACK的接收:對序號為n的分組的確認(rèn)用于累計確認(rèn)(cumulative acknowledgment)。即收到序號為n的確認(rèn)分組，則表明n之前的報文都正確收到，此時發(fā)送方將窗口基序號修改為n。

(3)超時事件:發(fā)送方使用一個定時器，它被最早的已發(fā)送但未被確認(rèn)的分組使用。如果超時發(fā)生，發(fā)送方將重發(fā)所有已發(fā)送過但還未被確認(rèn)過的分組。如果收到一個有效ACK，則定時器被重新啟動。

GBN協(xié)議的接收方動作很簡單，如果一個序號為n的分組被正確收到，并按序，則接收方為分組n發(fā)送一個ACK，并將分組中的數(shù)據(jù)交付到上層，在所有其他情況下，接收方丟棄該分組并為最近按序接收的分組重發(fā)ACK。

為研究方便，同時不影響實驗?zāi)康模诎l(fā)送方去除了上層調(diào)用檢查判斷發(fā)送窗口是否已滿的動作，簡化為發(fā)送方的skip動作，同時，發(fā)送方和接收方向上層遞交分組不予考慮，假定為收到即交付。GBN協(xié)議用Promela語言描述如下:

#define WIN 4 /*定義窗口大小*/

#define MAX 25/*定義發(fā)送報文計數(shù)最大值*/

chan s_r=[10] of {mtype，byte，byte};/*定義發(fā)送端到接收端傳輸通道*/

chan r_s=[10] of {mtype，byte，byte};/*定義接收端到發(fā)送端傳輸通道*/

mtype={mesg， ack， err};/*定義消息類型*/

proctype udt_sender() /*發(fā)送端進(jìn)程*/

{

byte s，r，swl;/*s為要發(fā)送的報文的序號，r為確認(rèn)報文的序號，swl為滑動窗口下限*/

swl = 0; /*窗口初始化*/

do::swl = swl;

progress:s = swl; /*將要發(fā)送報文指針移到窗口頭*/

progress1: if

::s_r!mesg(0，s)-> /*成功發(fā)送正確報文*/

(swl<=ss = (s+1)%MAX;/*s后移*/

if

::goto progress1; /*在窗口內(nèi)連續(xù)發(fā)送*/

::skip/*也可以不發(fā)送*/

fi;

::s_r!err(s，0) -> /*發(fā)送的報文在傳輸通道中出錯*/

(swl<=ss = (s+1)%MAX;

if

::goto progress1;

::skip

fi;

::skip -> /*報文在傳輸通道中丟失*/

(swl<=ss = (s+1)%MAX;

if

::goto progress1;

::skip

fi;

fi;

if

::timeout -> goto progress /*超時，從超時報文開始重發(fā)*/

::r_s?err(0，r) -> skip /*收到錯誤報文不工作*/

::r_s?ack(r，0) ->/*收到正確應(yīng)答報文*/

if

::(r skip /*確認(rèn)序號低于窗口下限*/

::(r>s) -> skip /*高于已發(fā)送報文最大值*/

::(swl<=r<=s) -> /*正確確認(rèn)*/

swl = r;/*移動窗口*/

goto progress; /*繼續(xù)發(fā)送*/

fi;

fi;

od

}

proctype udt_receiver()/*接收端進(jìn)程*/

{

byte t，es;/*t為接收報文的序號，es為期望收到的報文序號*/

es = 0; /*初始化*/

do

::s_r?mesg(0，t) ->/*收到正確報文*/

if

::(t==es)-> /*收到報文為所期望報文*/

progress2:es = (es + 1)%MAX;/*更新期望值*/

if

::r_s!ack(es，0) /*發(fā)送確認(rèn)*/

::r_s!err(0，es) /*發(fā)送的確認(rèn)報文在傳輸通道中出錯*/

::skip /*確認(rèn)報文在傳輸通道中丟失*/

fi

::(t!=es)->/*收到無效報文*/

if

::r_s!ack(es，0)/*重發(fā)確認(rèn)*/

::r_s!err(0，es) /*發(fā)送的確認(rèn)報文在傳輸通道中出錯*/

::skip /*確認(rèn)報文在傳輸通道中丟失*/

fi

fi

::s_r?err(t，0)->/*收到的報文出錯*/

if

::r_s!ack(es，0)/*重發(fā)確認(rèn)*/

::r_s!err(0，es) /*發(fā)送的確認(rèn)報文在傳輸通道中出錯*/

::skip /*確認(rèn)報文在傳輸通道中丟失*/

fi

od

}

init

{ /*啟動進(jìn)程*/

run udt_sender();

run udt_receiver();

}

本協(xié)議描述在xspin工具下運(yùn)行正常，經(jīng)仿真驗證，驗證了該描述的正確性。

3 問題和建議

3.1 問題的提出

在分析驗證GBN協(xié)議的過程中，我們發(fā)現(xiàn)，在確保協(xié)議正確性方面單純依靠工具會產(chǎn)生一些問題:

(1)書寫形式化描述同使用c、delphi等高級語言編程有很多類似的方面，只是語法更簡單，為處理方便和適應(yīng)形式化描述語言，協(xié)議分析驗證人員常常(或者必須)簡化或忽略某些操作，如本文對發(fā)送方同上層交互的簡化。這些簡化或忽略掉的操作是否不重要而可以被簡化或忽略?簡化或忽略掉這些操作是否會產(chǎn)生問題?這些問題單純依靠工具無法解決。

(2)當(dāng)研究人員分析了協(xié)議并使用形式化描述語言編寫出一個形式化描述，并用spin進(jìn)行了驗證，窮舉了所有的狀態(tài)空間，于是就認(rèn)為協(xié)議百分之百正確。事實上，研究人員只是證明了自己寫的形式化描述(或程序)在spin這個解釋器上運(yùn)行沒有問題，并不能保證協(xié)議的正確性。有這樣一種可能:某研究人員設(shè)計了一個協(xié)議，協(xié)議分析研究人員根據(jù)這個協(xié)議編寫了形式化描述，驗證沒問題，但事實上這個形式化描述所代表的協(xié)議同研究人員設(shè)計的協(xié)議可能根本不是同一個，而是協(xié)議分析研究人員根據(jù)自己的理解所產(chǎn)的“協(xié)議”。這樣，如何確保協(xié)議分析人員的“協(xié)議”同設(shè)計人員的“協(xié)議”之間的一致性?單純依靠工具無法解決。

(3)形式化描述語言往往語法較簡單，數(shù)據(jù)類型少，優(yōu)點是可以很快掌握，但存在問題就是往往表現(xiàn)不了太細(xì)節(jié)的內(nèi)容，只能對被驗證系統(tǒng)作簡化，簡化后的系統(tǒng)往往因不能處理細(xì)致的問題而沒有實用價值，因此，即使驗證了形式化描述的正確性也只是說明簡化系統(tǒng)正確，但實際的系統(tǒng)是否正確，不能肯定。如何確保形式化描述系統(tǒng)同實際應(yīng)用系統(tǒng)的一致性?同樣單純依靠工具無法解決。

如果spin工具生成的代碼能同用戶的實際程序相媲美，那么上面的問題就能解決，遺憾的是目前的工具在代碼自動生成方面還不是很理想，例如生成代碼往往比較長，可讀性差，等等，最重要的是與實際系統(tǒng)性能相差甚遠(yuǎn)，而現(xiàn)在似乎也看不到在將來自動生成的代碼能達(dá)到完成實際功能的希望。

3.2 具體建議

當(dāng)開發(fā)一個新的系統(tǒng)時，在軟件工程上需要確保最終生成的實際系統(tǒng)與用戶需求的一致，協(xié)議設(shè)計分析同樣如此，必須保證最終在實際系統(tǒng)中運(yùn)行的協(xié)議同用戶需求一致才能夠滿足要求，即保證下面的等式成立:

實際系統(tǒng)=用戶需求

但用戶需求的原始描述往往比較隨意，而實際開發(fā)的系統(tǒng)往往代碼冗長，分析源代碼不便，因而通過分析源代碼保證上述等式成立不可行，而通過軟件測試的方法也比較難以保證所有情況都考慮到，難以有效判斷上述等式是否成立。形式化描述的抽象性介于用戶需求和實際系統(tǒng)二者之間，具有比程序更好的可讀性又不像原始描述那樣隨意，因此，為提高協(xié)議開發(fā)的正確性，通過形式化描述在用戶需求原始描述與程序代碼之間加入了一個變換、緩沖，從而有助于分析判斷，即下面的等式:

實際系統(tǒng)=形式化描述=用戶需求

3.2中提出的第3個問題，如何確保形式化描述系統(tǒng)同實際應(yīng)用系統(tǒng)的一致性，即如何確保前一個“=”成立，第2個問題，如何確保協(xié)議分析人員的“協(xié)議”同設(shè)計人員的“協(xié)議”之間的一致性，即如何確保后一個“=”成立，第1個問題，如何判斷簡化或忽略掉的操作不重要，即如何確保簡化或忽略掉一些操作后上述兩個“=”仍然成立。

協(xié)議分析驗證工具本身并不能解答這些問題，它僅僅為研究人員提供了一個能夠?qū)π问交枋稣Z言進(jìn)行編輯、編譯、運(yùn)行的可視化工具，方便研究人員完成形式化描述并對該形式化描述進(jìn)行檢驗驗證，其他的問題必須靠研究人員自身解決，因此，提出如下建議:

(1)在用戶需求到形式化描述的過程中，研究人員必須慎重判斷協(xié)議中的各種操作，盡量少的簡化和省略操作，盡力去理解設(shè)計人員開發(fā)的協(xié)議，即盡可能完全地理解用戶需求，從而人工保證形式化描述=用戶需求。

(2)在協(xié)議驗證過程中，如有可能，研究人員必須詳細(xì)觀察協(xié)議在實際系統(tǒng)中的運(yùn)行，從而判斷協(xié)議執(zhí)行中的操作和其重要性，盡量保證簡化系統(tǒng)能夠反映實際系統(tǒng)的主要特性和操作;而在協(xié)議開發(fā)過程中，在應(yīng)用到實際系統(tǒng)時必須使程序與形式化描述盡量一致，從而人工保證形式化描述=實際系統(tǒng)。

在執(zhí)行上述兩項建議后，協(xié)議分析驗證人員能夠以人工方式保證實際系統(tǒng)=形式化描述=用戶需求，從而能夠正確驗證已經(jīng)應(yīng)用的協(xié)議或者開發(fā)新的協(xié)議并確保新協(xié)議正確應(yīng)用。

4 結(jié)語

論文簡單介紹了協(xié)議分析驗證工具SPIN，并利用其對GBN協(xié)議進(jìn)行了分析驗證，在此過程中發(fā)現(xiàn)了協(xié)議分析工具的局限性，提出了相關(guān)問題，并對如何解決這些問題給出了具體建議，為協(xié)議開發(fā)和驗證人員在研究過程中解決問題提供幫助。如何為研究人員提供更加方便、直觀的輔助從而減少研究過程中人為原因造成的不一致是今后協(xié)議分析驗證工具的一個重要的發(fā)展方向。

參考文獻(xiàn)

[1] 古天龍，蔡國永. 網(wǎng)絡(luò)協(xié)議的形式化分析與設(shè)計[M]. 北京:電子工業(yè)出版社，2003.

[2]葉新銘，郝松俠. IPv6鄰居發(fā)現(xiàn)協(xié)議的形式化驗證[J]. 軟件學(xué)報，2005(6).

[3] 庫羅斯[美]等著. 陳鳴，李兵，賈永興 譯. 計算機(jī)網(wǎng)絡(luò)-自頂向下方法與Internet特色(第三版)[M].北京:機(jī)械工業(yè)出版社，2009.