網(wǎng)絡(luò)協(xié)議工程SPIN實(shí)驗(yàn)報(bào)告

1、網(wǎng)絡(luò)協(xié)議工程SPIN實(shí)驗(yàn)報(bào)告摘要：本文主要介紹了一種基于模型檢測(cè)的協(xié)議自動(dòng)分析工具SPIN的使用。對(duì)經(jīng)典的AB協(xié)議在理想狀態(tài)、信道有誤碼無(wú)丟失和信道有誤碼有丟失三種不同環(huán)境中分別進(jìn)行建模，并運(yùn)用SPIN進(jìn)行自動(dòng)分析。在信道有誤碼有丟失的情況中，我們分別設(shè)置了兩種錯(cuò)誤，以進(jìn)一步觀察協(xié)議的運(yùn)行，分析協(xié)議存在的問(wèn)題。從而加深對(duì)協(xié)議驗(yàn)證技術(shù)和形式化描述技術(shù)的認(rèn)識(shí)和理解，進(jìn)一步掌握運(yùn)用PROMELA語(yǔ)言對(duì)協(xié)議進(jìn)行建模，同時(shí)掌握SPIN的基本操作，熟悉運(yùn)用SPIN對(duì)網(wǎng)絡(luò)協(xié)議進(jìn)行分析，提高實(shí)驗(yàn)?zāi)芰?。關(guān)鍵詞：模型檢測(cè)；AB協(xié)議；SPIN。0.引言隨著計(jì)算機(jī)通信與網(wǎng)絡(luò)技術(shù)的迅猛發(fā)展，網(wǎng)絡(luò)技術(shù)在人們?nèi)粘５墓ぷ?、學(xué)

2、習(xí)和生活的各個(gè)方面都得到了普遍地運(yùn)用。各種網(wǎng)絡(luò)通信系統(tǒng)在提供越來(lái)越豐富的功能的同時(shí)，其設(shè)計(jì)和實(shí)現(xiàn)也日益復(fù)雜。面對(duì)復(fù)雜網(wǎng)絡(luò)系統(tǒng)的挑戰(zhàn)，傳統(tǒng)的自然語(yǔ)言進(jìn)行的協(xié)議描述，雖然具有表達(dá)能力強(qiáng)、可讀性好、方便的優(yōu)點(diǎn)，但是存在不嚴(yán)格、不精確、沒(méi)有描述標(biāo)準(zhǔn)和存有二義性等缺點(diǎn)。形式化方法使得對(duì)網(wǎng)絡(luò)通信系統(tǒng)的描述、實(shí)現(xiàn)和測(cè)試變得容易，在對(duì)于協(xié)議實(shí)現(xiàn)、測(cè)試的自動(dòng)化和協(xié)議驗(yàn)證上得到了廣泛運(yùn)用。本文主要介紹一種基于模型檢測(cè)的協(xié)議自動(dòng)分析工具SPIN及其在分析網(wǎng)絡(luò)協(xié)議中的應(yīng)用。1.SPIN概述隨著計(jì)算機(jī)通信與網(wǎng)絡(luò)技術(shù)的迅猛發(fā)展，網(wǎng)絡(luò)技術(shù)在人們?nèi)粘５墓ぷ?、學(xué)習(xí)和生活的各個(gè)方面都得到了普遍運(yùn)用。各種網(wǎng)絡(luò)通信系統(tǒng)在提供越來(lái)越豐

3、富的功能的同時(shí)，其設(shè)計(jì)和實(shí)現(xiàn)也日益復(fù)雜。面對(duì)復(fù)雜網(wǎng)絡(luò)系統(tǒng)的挑戰(zhàn)，傳統(tǒng)的自然語(yǔ)言進(jìn)行的協(xié)議描述，雖然具有表達(dá)能力強(qiáng)、可讀性好、方便等優(yōu)點(diǎn)，但是存在不嚴(yán)格、不精確、沒(méi)有描述標(biāo)準(zhǔn)和存有二義性等缺點(diǎn)。形式化方法使得對(duì)網(wǎng)絡(luò)通信系統(tǒng)的描述、實(shí)現(xiàn)和測(cè)試變得容易，在對(duì)于協(xié)議實(shí)現(xiàn)、測(cè)試的自動(dòng)化和協(xié)議驗(yàn)證上得到了廣泛運(yùn)用。本文主要介紹一種基于模型檢測(cè)的協(xié)議自動(dòng)分析工具SPIN及其應(yīng)用。1.1 SPIN概述SPIN(Simple PROMELA Interpreter)是一種用丁對(duì)并發(fā)系統(tǒng)驗(yàn)證模型檢測(cè)器，采用深度優(yōu)先搜索算法，偏序化簡(jiǎn)和on-the-fly策略從不同的角度來(lái)解決模型檢測(cè)方法中普遍存在的狀態(tài)空間爆炸問(wèn)

4、題，其適合對(duì)協(xié)議驗(yàn)證。SPIN支持隨機(jī)、交互和指導(dǎo)性的自動(dòng)機(jī)驗(yàn)證，它主要針對(duì)設(shè)計(jì)規(guī)范進(jìn)行檢測(cè)。最早是由貝爾實(shí)驗(yàn)室的形式化方法與驗(yàn)證小組于1980年開(kāi)始開(kāi)發(fā)的。1995年偏序簡(jiǎn)約和線性時(shí)態(tài)邏輯轉(zhuǎn)換的引入使得SPIN的功能進(jìn)一步擴(kuò)大。2001年推出的SPIN4.0版本支持C代碼的植入，應(yīng)用的靈活性進(jìn)一步增強(qiáng)。隨后2003年推出的SPIN4.1版本加入了深度優(yōu)先搜索算法，2009年連續(xù)推出SPIN5.2版本，這使得SPIN的發(fā)展又上一個(gè)新臺(tái)階。NASA使用SPIN檢測(cè)在1996年火星探測(cè)者所存在的錯(cuò)誤，結(jié)果發(fā)現(xiàn)一些錯(cuò)誤是可以在發(fā)射之前就可以被檢測(cè)并改正的。SPIN從此就被用來(lái)檢測(cè)土星火箭控制軟件和一

5、些應(yīng)用與外層空間的程序。因SPIN有良好的算法設(shè)計(jì)和非凡的檢測(cè)能力，得到了ACM(Association for Computing Machinery)(世界最早的專業(yè)計(jì)算機(jī)協(xié)會(huì))的認(rèn)可，在2001年授予SPIN的開(kāi)發(fā)者Holzmann享有聲望的軟件系統(tǒng)獎(jiǎng)。迄今為止SPIN也是唯一獲得ACM軟件系統(tǒng)獎(jiǎng)的模型檢測(cè)工具。SPIN通過(guò)模仿系統(tǒng)的執(zhí)行并產(chǎn)生C程序，探測(cè)系統(tǒng)的狀態(tài)空間，最終驗(yàn)證系統(tǒng)的屬性是否滿足，如不滿足，通過(guò)提供系統(tǒng)軌跡的形式幫助使用者找出違反正確性屬性的狀態(tài)。SPIN作為一種形式化自動(dòng)驗(yàn)證工具，其目的是：提供系統(tǒng)建模語(yǔ)言，用于直觀、明確地描述系統(tǒng)模型規(guī)約，而不考慮具體實(shí)現(xiàn)細(xì)節(jié)；功能

6、強(qiáng)大而簡(jiǎn)明的描述系統(tǒng)應(yīng)滿足性質(zhì)屬性要求的邏輯表示法：提供一套驗(yàn)證系統(tǒng)建模邏輯一致性及系統(tǒng)是否滿足所要驗(yàn)證性質(zhì)的方法。它以PROMELA為輸入語(yǔ)言，用線性時(shí)態(tài)邏輯(LTL)公式描述系統(tǒng)必須滿足的性質(zhì)。SPIN可以對(duì)大型的協(xié)議系統(tǒng)進(jìn)行有效的正確性分析，即使這個(gè)系統(tǒng)覆蓋了最大限度的狀態(tài)空間。SPIN首先從一個(gè)描述的協(xié)議系統(tǒng)的高層模型規(guī)格開(kāi)始，經(jīng)分析沒(méi)有語(yǔ)法錯(cuò)誤后，對(duì)系統(tǒng)的交互進(jìn)行模擬，直到確認(rèn)系統(tǒng)設(shè)計(jì)擁有預(yù)期的行為；然后，SPIN將產(chǎn)生一個(gè)明C語(yǔ)言描述的驗(yàn)證程序，經(jīng)檢驗(yàn)器編譯后被執(zhí)行，執(zhí)行中如果發(fā)現(xiàn)了違背正確性說(shuō)明的任何反例，則可反饋給交互模擬機(jī)，通過(guò)重現(xiàn)細(xì)節(jié)剔除引起錯(cuò)誤的原因。圖1-1描述了SPI

7、N模擬和檢測(cè)的過(guò)程。PROMELA解析器LTL公式解析和轉(zhuǎn)換器SPIN語(yǔ)法錯(cuò)誤報(bào)告驗(yàn)證機(jī)產(chǎn)生器交互模擬模型優(yōu)化測(cè)試器執(zhí)行on-the-fly驗(yàn)證反例圖1-1 SPIN模擬和檢測(cè)的過(guò)程1.2 SPIN安裝及使用SPIN可以在很多平臺(tái)上運(yùn)行，具有很多版本，我們?cè)谶@個(gè)實(shí)驗(yàn)中是在Windows7 64位操作系統(tǒng)中，基于Cygwin linux模擬器中實(shí)現(xiàn)的，下面是簡(jiǎn)要的安裝過(guò)程。1.軟件準(zhǔn)備：（1）在 distribution, with sources版本，最新版本是6.44，下載的文件名為：spin644.tar.gz。解壓后，里面文件內(nèi)容：（2）下載并運(yùn)行cygwin軟件，選擇64位window

8、s版本。選擇默認(rèn)參數(shù)安裝。需要注意以下幾點(diǎn)：a.選擇下載站點(diǎn)要選擇等國(guó)內(nèi)鏡像站點(diǎn)，加快下載速度。b.需要選擇相應(yīng)的安裝組件：(binutils 、bison、 byacc、xinit、x-org-server、m4、tcl等)選擇紅色框部分，展開(kāi) 分別選擇：binutils 、bison、 byacc繼續(xù)選擇：繼續(xù)選擇：make 退到上一層，選擇展開(kāi)x11選項(xiàng)：繼續(xù)選擇：下面2項(xiàng) 然后，退回上層，搜素m4在結(jié)果中選擇安裝搜素tcl，選擇相應(yīng)包（tcl是運(yùn)行圖形界面ISPIN的必須環(huán)境）。點(diǎn)擊下一步，等待安安裝完成。最后選擇創(chuàng)建桌面和開(kāi)始菜單文件，完成安裝。3）安裝完cygwin后，在系統(tǒng)盤(pán)（C

9、盤(pán)）會(huì)有文件夾，進(jìn)入：c:/cygwin64/bin中，將第一步已解壓的SPIN文件夾復(fù)制進(jìn)來(lái)，并改名為Spin1。進(jìn)入Spin1文件夾中的iSpin文件夾，復(fù)制ispin.tcl至外面的bin目錄中，并去掉.tcl后綴。c.編譯配置ISPIN安裝完cygwin后，先在windows7命令行運(yùn)行：C:>set CYGWIN=tty notitle glob，打開(kāi)cygwin的控制臺(tái)程序：進(jìn)入到spin源碼目錄中c:/cygwin64/bin/spin1/src然后進(jìn)行make：（如果編譯不成功，往往因?yàn)閏ygwin編譯環(huán)境沒(méi)裝好，重新檢查安裝環(huán)節(jié)組件的選擇）輸入命令：make f mak

10、efile成功后，src目錄里會(huì)產(chǎn)生spin.exe，將其復(fù)制到bin目錄中。測(cè)試tcl環(huán)境(如果找不到相應(yīng)文件，則無(wú)法運(yùn)行ISPIN，重新檢查安裝環(huán)節(jié)tcl組件的選擇)輸入命令：Which tclsh輸入命令：Which wishd.運(yùn)行ISPIN運(yùn)行開(kāi)始->cygwin-x->xwin server桌面右下角會(huì)出現(xiàn)當(dāng)前的x server的虛擬桌面編號(hào)（:2.0）在cygwin的控制臺(tái)中指定ISPIN運(yùn)行界面的虛擬桌面編號(hào)輸入命令：export DISPLAY=:2.0運(yùn)行ISPIN輸入命令：ispin這樣就可以使用ISPIN。2.實(shí)例分析本次實(shí)驗(yàn)主要分析AB協(xié)議，分別針對(duì)理想狀

11、態(tài)、信道有誤碼無(wú)丟失和信道有誤碼有丟失，三種不同的通信環(huán)境，設(shè)計(jì)測(cè)試三組實(shí)驗(yàn)。在第三組實(shí)驗(yàn)過(guò)程中，又進(jìn)行了協(xié)議的兩種錯(cuò)誤處理。2.1AB協(xié)議簡(jiǎn)介AB(Alternating Bit)協(xié)議是最早的端到端通信協(xié)議之一。在AB協(xié)議系統(tǒng)中，包含有發(fā)送端和接收端兩個(gè)實(shí)體。發(fā)送端協(xié)議實(shí)體從發(fā)送方獲取一個(gè)報(bào)文，將序號(hào)寄存器值賦給報(bào)文，然后向接收端實(shí)體發(fā)出報(bào)文，發(fā)送方發(fā)出報(bào)文之后啟動(dòng)超時(shí)計(jì)時(shí)器，等待確認(rèn)報(bào)文。如果在給定的時(shí)間內(nèi)沒(méi)有收到確認(rèn)報(bào)文，則重發(fā)該報(bào)文。如果收到確認(rèn)報(bào)文，其序號(hào)與發(fā)出報(bào)文序號(hào)相同，則序號(hào)寄存器的內(nèi)容加l模2，然后發(fā)送端實(shí)體從發(fā)送方用戶獲取下一個(gè)報(bào)文；如果收到否定的確認(rèn)報(bào)文，則重發(fā)該報(bào)文；接

12、收端協(xié)議實(shí)體在收到報(bào)文后，如果確認(rèn)報(bào)文無(wú)錯(cuò)誤，并且序號(hào)和序號(hào)寄存器的值相等，則向發(fā)送端實(shí)體發(fā)送確認(rèn)報(bào)文(認(rèn)可報(bào)文的序號(hào)值等于接收?qǐng)?bào)文的序號(hào)值)，然后將報(bào)文遞交給接收方用戶，序號(hào)寄存器的內(nèi)容加l模2。如果接收的報(bào)文有錯(cuò)誤，或者序號(hào)不正確，則發(fā)送否定確認(rèn)報(bào)文。2.2理想狀態(tài)下的AB協(xié)議實(shí)驗(yàn)在理想狀態(tài)下，信道沒(méi)有誤碼，沒(méi)有丟失，接收方有無(wú)限接收能力。這種狀態(tài)下，協(xié)議比較簡(jiǎn)單，一方發(fā)送，一方接收，不設(shè)超時(shí)計(jì)時(shí)器，不進(jìn)行報(bào)文確認(rèn)。下面是協(xié)議的PROMELA描述模型。1 #define MAXSEQ 32 chan SenderToReceiver=1 ofint; /只含有1個(gè)int類型的通道34 pr

13、octype SENDER() /發(fā)送方5 6int seq=0;7end:do8:SenderToReceiver!seq; /發(fā)送序號(hào)9 process:seq=(seq+1)%MAXSEQ; /10od;1112 1314 proctype RECEIVER() /接收方15 16int Data;17end1:do18:SenderToReceiver?Data; /從通道接收數(shù)據(jù)19od;20 21 /-開(kāi)始運(yùn)行協(xié)議-22 init23 24atomic /原子操作2526run SENDER();27run RECEIVER();2829 將上述代碼保存為RTD1.pml，在ISP

14、IN中打開(kāi)，點(diǎn)擊Syntax Check進(jìn)行語(yǔ)法錯(cuò)誤檢測(cè)，如圖所示，沒(méi)有語(yǔ)法錯(cuò)誤。然后選擇verification選項(xiàng)卡，進(jìn)行模型驗(yàn)證，模型驗(yàn)證分成三塊，safety、liveness、以及LTL never claims。剛開(kāi)始我們先對(duì)程序進(jìn)行安全性和可活動(dòng)性驗(yàn)證，下面截圖中用的是默認(rèn)勾選的選項(xiàng)，第一個(gè)表示死鎖，進(jìn)程無(wú)法執(zhí)行下去，第二個(gè)表示程序的斷言沖突（在RTD1.pml中不包含斷言），第三個(gè)是允許循環(huán)，就是允許只有一個(gè)進(jìn)程一直處于活動(dòng)狀態(tài)，而另一個(gè)不動(dòng)。點(diǎn)擊run進(jìn)行驗(yàn)證，如圖所示，沒(méi)有存在error。Unreached說(shuō)明兩個(gè)進(jìn)程一直在循環(huán)運(yùn)行。點(diǎn)擊Simulate/Replay，進(jìn)行

15、模擬重放，點(diǎn)擊(Re)Run，可以形象地觀察協(xié)議運(yùn)行過(guò)程。發(fā)送方按0,1,2有序發(fā)送，接收方按0,1,2有序接收。2.3 信道有誤碼、無(wú)丟失下的AB協(xié)議實(shí)驗(yàn)在此實(shí)驗(yàn)中，我們考慮收發(fā)信道都產(chǎn)生誤碼，但沒(méi)有發(fā)生丟包的情形。分別用進(jìn)程SENDER和RECEIVER來(lái)對(duì)AB協(xié)議的發(fā)送端和接收端進(jìn)行建模：通過(guò)進(jìn)程SENDER的發(fā)送語(yǔ)句“OutCh!Msg(SendData,SendSeq)”和“OutCh!Err(8,8)”分別模擬正確傳送和誤碼兩種情況；通過(guò)進(jìn)程RECEIVER的發(fā)送語(yǔ)句“OutCh!Ack(ReceivedSeq,0)”、OutCh!Nak(ReceivedSeq,0)和“OutCh

16、!Err(8,8)”來(lái)分別模擬確認(rèn)報(bào)文、否定確認(rèn)報(bào)文和回執(zhí)報(bào)文發(fā)送誤碼三種情況。在SENDER和RECEIVER進(jìn)程中使用了assert語(yǔ)句來(lái)檢驗(yàn)在可能會(huì)發(fā)生任意的消息丟失的情況下，數(shù)據(jù)是否能全部按順序正確地傳送到接收端。在SENDER和RECEIVER進(jìn)程中使剛progress狀態(tài)標(biāo)記兩端傳送確實(shí)的數(shù)據(jù)所必須要執(zhí)行的語(yǔ)句。因?yàn)橛锌赡馨l(fā)送端和接收端只在某些無(wú)效的狀態(tài)中循環(huán)，使用progress標(biāo)記可以在檢測(cè)過(guò)程中檢測(cè)出沒(méi)有任何實(shí)質(zhì)意義的不可推進(jìn)的循環(huán)。下面是協(xié)議的PROMELA描述模型。1 #define MAXSEQ 523 mtype=Msg,Ack,Nak,Err;45 chan Sen

17、derToReceiver=1 of mtype,byte,byte;6 chan ReceiverToSender=1 of mtype,byte,byte;78 proctype SENDER(chan InCh,OutCh)9 10 byte SendData;/發(fā)送的數(shù)據(jù)11 byte SendSeq;/發(fā)送序號(hào)12 byte ReceivedSeq;/接收序號(hào)13 SendData=MAXSEQ-1;/下一個(gè)要發(fā)送的序號(hào)14 do15:SendData=(SendData+1)%MAXSEQ; /下一個(gè)消息16 again:if17:OutCh!Msg(SendData,SendSe

18、q) /正確發(fā)送數(shù)據(jù)18:OutCh!Err(8,8) /出現(xiàn)誤碼19 fi;2021if22:InCh?Nak(ReceivedSeq,0)->23 end:goto again /收到否定確認(rèn)，重傳24:InCh?Err(8,8)-> goto again /收到ACK誤碼，重傳25:InCh?Ack(ReceivedSeq,0)-> /收到肯定確認(rèn)26if2728:(ReceivedSeq=SendSeq)->goto progress /確認(rèn)號(hào)正確，傳下一報(bào)文29:(ReceivedSeq!=SendSeq)->30 end1:goto again /確認(rèn)

19、號(hào)有誤，重傳31fi32fi;33 progress:SendSeq=1-SendSeq; /產(chǎn)生下一個(gè)報(bào)文序號(hào)34 od;35 3637 proctype RECEIVER(chan InCh,OutCh)38 39 byte ReceivedData; /接收的數(shù)據(jù)40 byte ReceivedSeq; /接收的序號(hào)41 byte ExpectedData; /期望的數(shù)據(jù)42 byte ExpectedSeq; /期望的序號(hào)4344 do45:InCh?Msg(ReceivedData,ReceivedSeq)->46if47:(ReceivedSeq=ExpectedSeq)-&

20、gt; /數(shù)據(jù)按序到達(dá)，發(fā)送確認(rèn)報(bào)文48assert(ReceivedData=ExpectedData); /檢驗(yàn)數(shù)據(jù)是否能按順序傳送到接收端49 progress:ExpectedSeq=1-ExpectedSeq;50ExpectedData=(ExpectedData+1)%MAXSEQ;51if52:OutCh!Ack(ReceivedSeq,0); /ACK報(bào)文正確53:OutCh!Err(8,8); /模擬ACK報(bào)文誤碼54ExpectedSeq=1-ExpectedSeq;55ExpectedData=(ExpectedData+4)%MAXSEQ;56fi5758:(Rece

21、ivedSeq!=ExpectedSeq) -> 59if60:OutCh!Nak(ReceivedSeq,0); /數(shù)據(jù)不按序到達(dá)，發(fā)送否定確認(rèn)報(bào)文61:OutCh!Err(8,8); /模擬ACK報(bào)文誤碼62fi63fi64:InCh?Err -> OutCh!Nak(ReceivedSeq,0); /數(shù)據(jù)錯(cuò)誤，發(fā)送否定確認(rèn)報(bào)文65 od;66 676869 init70 71atomic /原子操作，執(zhí)行過(guò)程不允許打斷7273run SENDER(ReceiverToSender,SenderToReceiver);/發(fā)送者74run RECEIVER(SenderToRec

22、eiver,ReceiverToSender); /接收者7576 將上述代碼保存為RTD2.pml，在ISPIN中打開(kāi)，點(diǎn)擊Syntax Check進(jìn)行語(yǔ)法錯(cuò)誤檢測(cè)，沒(méi)有語(yǔ)法錯(cuò)誤。然后選擇verification選項(xiàng)卡，進(jìn)行模型驗(yàn)證，點(diǎn)擊run進(jìn)行驗(yàn)證，如圖所示，沒(méi)有存在error。Unreached說(shuō)明兩個(gè)進(jìn)程一直在循環(huán)運(yùn)行。點(diǎn)擊Simulate/Replay，進(jìn)行模擬重放，點(diǎn)擊(Re)Run，可以形象地觀察協(xié)議運(yùn)行過(guò)程。從圖中，我們可以直觀的看到否定確認(rèn)、正確確認(rèn)、回執(zhí)產(chǎn)生誤碼和發(fā)送報(bào)文產(chǎn)生誤碼的情況。否定確認(rèn)確認(rèn)報(bào)文回執(zhí)誤碼發(fā)送誤碼2.4信道有誤碼、有丟失下的AB協(xié)議實(shí)驗(yàn)在此實(shí)驗(yàn)中，我

23、們考慮收發(fā)信道都產(chǎn)生誤碼，并且都有發(fā)生丟包的情形。分別用進(jìn)程SENDER和RECEIVER來(lái)對(duì)AB協(xié)議的發(fā)送端和接收端進(jìn)行建模：通過(guò)進(jìn)程SENDER的發(fā)送語(yǔ)句“OutCh!Msg(SendData,SendSeq)”、“OutCh!Err(8,8)”和“skip”分別模擬正確傳送、誤碼和丟包三種情況；通過(guò)進(jìn)程RECEIVER的發(fā)送語(yǔ)句“OutCh!Ack(ReceivedSeq,0)”、“OutCh!Nak(ReceivedSeq,0)”、“OutCh!Err(8,8)”和“skip”來(lái)分別模擬確認(rèn)報(bào)文、否定確認(rèn)報(bào)文、回執(zhí)報(bào)文發(fā)送誤碼和回執(zhí)報(bào)文丟失三種情況。進(jìn)程RECEIVER中，對(duì)正確接收的

24、報(bào)文回執(zhí)時(shí)，產(chǎn)生回執(zhí)報(bào)文誤碼“OutCh!Err(8,8) ”和丟包“skip”的情況，應(yīng)該用“ExpectedSeq=1-ExpectedSeq;ExpectedData=(ExpectedData+4)%MAXSEQ;”，來(lái)還原因前一個(gè)數(shù)據(jù)包正確接收而更改的“ExpectedSeq”和“ExpectedData”的值，否則會(huì)因?yàn)槠谕邮招蛱?hào)與實(shí)際接收序號(hào)不一致而一直處于回執(zhí)“OutCh!Nak(ReceivedSeq,0)”的情況。在SENDER和RECEIVER進(jìn)程中使用了assert語(yǔ)句來(lái)檢驗(yàn)在可能會(huì)發(fā)生任意的消息丟失的情況下，數(shù)據(jù)是否能全部按順序正確地傳送到接收端。在SENDER和R

25、ECEIVER進(jìn)程中使剛progress狀態(tài)標(biāo)記兩端傳送確實(shí)的數(shù)據(jù)所必須要執(zhí)行的語(yǔ)句。因?yàn)橛锌赡馨l(fā)送端和接收端只在某些無(wú)效的狀態(tài)中循環(huán)，使用progress標(biāo)記可以在檢測(cè)過(guò)程中檢測(cè)出沒(méi)有任何實(shí)質(zhì)意義的不可推進(jìn)的循環(huán)。在此實(shí)驗(yàn)中，我們分別模擬了兩種錯(cuò)誤情況：一是發(fā)送方對(duì)否定確認(rèn)報(bào)文的忽略，二是接收方在回執(zhí)發(fā)生丟包時(shí)，未及時(shí)還原期望接收數(shù)據(jù)和期望接收序號(hào)。下面是協(xié)議的PROMELA描述模型。1 #define MAXSEQ 523 mtype=Msg,Ack,Nak,Err;45 chan SenderToReceiver=1 of mtype,byte,byte;6 chan ReceiverT

26、oSender=1 of mtype,byte,byte;78 proctype SENDER(chan InCh,OutCh)9 10 byte SendData;/發(fā)送的數(shù)據(jù)11 byte SendSeq;/發(fā)送序號(hào)12 byte ReceivedSeq;/接收序號(hào)13 SendData=MAXSEQ-1;/下一個(gè)要發(fā)送的序號(hào)14 do15:SendData=(SendData+1)%MAXSEQ; /下一個(gè)消息16 again:if17:OutCh!Msg(SendData,SendSeq) /正確發(fā)送數(shù)據(jù)18:OutCh!Err(8,8) /出現(xiàn)誤碼19:skip /報(bào)文丟失20 fi

27、;2122if23:timeout -> goto again /超時(shí)重傳24:InCh?Nak(ReceivedSeq,0)->25 end:goto again /收到否定確認(rèn)，重傳26:InCh?Err(8,8)-> goto again /收到ACK誤碼，重傳27:InCh?Ack(ReceivedSeq,0)-> /收到肯定確認(rèn)28if2930:(ReceivedSeq=SendSeq)->goto progress /確認(rèn)號(hào)正確，傳下一報(bào)文31:(ReceivedSeq!=SendSeq)->32 end1:goto again /確認(rèn)號(hào)有誤，重

28、傳33fi34fi;35 progress:SendSeq=1-SendSeq; /產(chǎn)生下一個(gè)報(bào)文序號(hào)36 od;37 3839 proctype RECEIVER(chan InCh,OutCh)40 41 byte ReceivedData; /接收的數(shù)據(jù)42 byte ReceivedSeq; /接收的序號(hào)43 byte ExpectedData; /期望的數(shù)據(jù)44 byte ExpectedSeq; /期望的序號(hào)4546 do47:InCh?Msg(ReceivedData,ReceivedSeq)->48if49:(ReceivedSeq=ExpectedSeq)-> /

29、數(shù)據(jù)按序到達(dá)，發(fā)送確認(rèn)報(bào)文50assert(ReceivedData=ExpectedData); /檢驗(yàn)數(shù)據(jù)是否能按順序傳送到接收端51 progress:ExpectedSeq=1-ExpectedSeq;52ExpectedData=(ExpectedData+1)%MAXSEQ;53if54:OutCh!Ack(ReceivedSeq,0); /ACK報(bào)文正確55:OutCh!Err(8,8); /模擬ACK報(bào)文誤碼，并還原期望的序號(hào)和數(shù)據(jù)56ExpectedSeq=1-ExpectedSeq;57ExpectedData=(ExpectedData+4)%MAXSEQ;58:skip

30、 /報(bào)文丟失，并還原期望的序號(hào)和數(shù)據(jù)59ExpectedSeq=1-ExpectedSeq;60ExpectedData=(ExpectedData+4)%MAXSEQ;61fi6263:(ReceivedSeq!=ExpectedSeq) -> 64if65:OutCh!Nak(ReceivedSeq,0); /數(shù)據(jù)不按序到達(dá)，發(fā)送否定確認(rèn)報(bào)文66:OutCh!Err(8,8); /模擬ACK報(bào)文誤碼67:skip /報(bào)文丟失68fi69fi70:InCh?Err(8,8) -> OutCh!Nak(ReceivedSeq,0); /數(shù)據(jù)錯(cuò)誤，發(fā)送否定確認(rèn)報(bào)文71 od;72 7

31、37475 init76 77atomic /原子操作，執(zhí)行過(guò)程不允許打斷7879run SENDER(ReceiverToSender,SenderToReceiver);/發(fā)送者80run RECEIVER(SenderToReceiver,ReceiverToSender); /接收者8182 將上述代碼保存為RTD3.pml，在ISPIN中打開(kāi)，點(diǎn)擊Syntax Check進(jìn)行語(yǔ)法錯(cuò)誤檢測(cè)，沒(méi)有語(yǔ)法錯(cuò)誤。然后選擇verification選項(xiàng)卡，進(jìn)行模型驗(yàn)證，點(diǎn)擊run進(jìn)行驗(yàn)證，如圖所示，沒(méi)有存在error。Unreached說(shuō)明兩個(gè)進(jìn)程一直在循環(huán)運(yùn)行。點(diǎn)擊Simulate/Replay

32、，進(jìn)行模擬重放，點(diǎn)擊(Re)Run，可以形象地觀察協(xié)議運(yùn)行過(guò)程。從圖中，我們可以直觀的看到丟包、否定確認(rèn)、正確確認(rèn)、回執(zhí)產(chǎn)生誤碼和發(fā)送報(bào)文產(chǎn)生誤碼的情況。丟包回執(zhí)誤碼發(fā)送誤碼正確確認(rèn)否定確認(rèn)2.4.1下面來(lái)觀察兩種錯(cuò)誤的處理。1.發(fā)送方對(duì)否定確認(rèn)報(bào)文的忽視如果我們修改25行中，對(duì)否定確認(rèn)報(bào)文正確的處理應(yīng)該是重傳，而改為忽視，不重傳，還是繼續(xù)發(fā)送下一個(gè)數(shù)據(jù)，則在進(jìn)行模型驗(yàn)證時(shí)，會(huì)產(chǎn)生一個(gè)錯(cuò)誤“assertion violated (ReceivedData=ExpectedData) (at depth 121)”，我們?cè)诔绦蛑械?0行用assert標(biāo)記進(jìn)行檢驗(yàn)數(shù)據(jù)是否能按順序傳送到接收端時(shí)，系

33、統(tǒng)產(chǎn)生違反這一檢測(cè)的錯(cuò)誤。在進(jìn)行Simulate/Replay，進(jìn)行模擬重放，在Mode選項(xiàng)頁(yè)中，會(huì)自動(dòng)勾選Guided，with trail，ISPIN會(huì)將錯(cuò)誤的運(yùn)行結(jié)果存儲(chǔ)到RTD3.pml.trail文件中，點(diǎn)擊(Re)Run進(jìn)行回放，在運(yùn)行到最后一步時(shí)，我們從變量窗口發(fā)現(xiàn)：RECEIVER(2):ExpectedData = 0RECEIVER(2):ExpectedSeq = 0RECEIVER(2):ReceivedData = 2RECEIVER(2):ReceivedSeq = 0SENDER(1):ReceivedSeq = 1SENDER(1):SendData = 2SENDER(1):SendSeq = 0對(duì)于接收者RECEIVER（）來(lái)說(shuō)，期望接收到的數(shù)據(jù)是0，但是實(shí)際接收到的數(shù)據(jù)為2，