網(wǎng)絡(luò)協(xié)議工程SPIN實驗報告

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

16、!Err(8,8)”來分別模擬確認(rèn)報文、否定確認(rèn)報文和回執(zhí)報文發(fā)送誤碼三種情況。在SENDER和RECEIVER進(jìn)程中使用了assert語句來檢驗在可能會發(fā)生任意的消息丟失的情況下，數(shù)據(jù)是否能全部按順序正確地傳送到接收端。在SENDER和RECEIVER進(jìn)程中使剛progress狀態(tài)標(biāo)記兩端傳送確實的數(shù)據(jù)所必須要執(zhí)行的語句。因為有可能發(fā)送端和接收端只在某些無效的狀態(tài)中循環(huán)，使用progress標(biāo)記可以在檢測過程中檢測出沒有任何實質(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ā)送序號12 byte ReceivedSeq;/接收序號13 SendData=MAXSEQ-1;/下一個要發(fā)送的序號14 do15:SendData=(SendData+1)%MAXSEQ; /下一個消息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)號正確，傳下一報文29:(ReceivedSeq!=SendSeq)->30 end1:goto again /確認(rèn)

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

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

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

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

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

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

25、ECEIVER進(jìn)程中使剛progress狀態(tài)標(biāo)記兩端傳送確實的數(shù)據(jù)所必須要執(zhí)行的語句。因為有可能發(fā)送端和接收端只在某些無效的狀態(tài)中循環(huán)，使用progress標(biāo)記可以在檢測過程中檢測出沒有任何實質(zhì)意義的不可推進(jìn)的循環(huán)。在此實驗中，我們分別模擬了兩種錯誤情況：一是發(fā)送方對否定確認(rèn)報文的忽略，二是接收方在回執(zhí)發(fā)生丟包時，未及時還原期望接收數(shù)據(jù)和期望接收序號。下面是協(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ā)送序號12 byte ReceivedSeq;/接收序號13 SendData=MAXSEQ-1;/下一個要發(fā)送的序號14 do15:SendData=(SendData+1)%MAXSEQ; /下一個消息16 again:if17:OutCh!Msg(SendData,SendSeq) /正確發(fā)送數(shù)據(jù)18:OutCh!Err(8,8) /出現(xiàn)誤碼19:skip /報文丟失20 fi

27、;2122if23:timeout -> goto again /超時重傳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)號正確，傳下一報文31:(ReceivedSeq!=SendSeq)->32 end1:goto again /確認(rèn)號有誤，重

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

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

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

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

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

33、統(tǒng)產(chǎn)生違反這一檢測的錯誤。在進(jìn)行Simulate/Replay，進(jìn)行模擬重放，在Mode選項頁中，會自動勾選Guided，with trail，ISPIN會將錯誤的運行結(jié)果存儲到RTD3.pml.trail文件中，點擊(Re)Run進(jìn)行回放，在運行到最后一步時，我們從變量窗口發(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對于接收者RECEIVER（）來說，期望接收到的數(shù)據(jù)是0，但是實際接收到的數(shù)據(jù)為2，