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

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

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

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

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

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

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

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

1.2 形式化描述語言Promela

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

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

2.1 GBN協(xié)議

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

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

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

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

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

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

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

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

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

#define MAX 25/*定義發(fā)送報(bào)文計(jì)數(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ā)送的報(bào)文的序號(hào)，r為確認(rèn)報(bào)文的序號(hào)，swl為滑動(dòng)窗口下限*/

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

do::swl = swl;

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

progress1: if

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

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

if

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

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

fi;

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

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

if

::goto progress1;

::skip

fi;

::skip -> /*報(bào)文在傳輸通道中丟失*/

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

if

::goto progress1;

::skip

fi;

fi;

if

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

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

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

if

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

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

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

swl = r;/*移動(dòng)窗口*/

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

fi;

fi;

od

}

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

{

byte t，es;/*t為接收?qǐng)?bào)文的序號(hào)，es為期望收到的報(bào)文序號(hào)*/

es = 0; /*初始化*/

do

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

if

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

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

if

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

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

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

fi

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

if

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

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

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

fi

fi

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

if

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

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

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

fi

od

}

init

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

run udt_sender();

run udt_receiver();

}

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

3 問題和建議

3.1 問題的提出

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

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

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

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

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

3.2 具體建議

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

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

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

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

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

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

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

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

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

4 結(jié)語

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

參考文獻(xiàn)

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

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

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