網(wǎng)絡(luò)協(xié)議工程SPIN實驗報告摘要：本文重要介紹了一種基于模型檢測的協(xié)議自動分析工具SPIN的使用。對經(jīng)典的AB協(xié)議在抱負(fù)狀態(tài)、信道有誤碼無丟失和信道有誤碼有丟失三種不同環(huán)境中分別進(jìn)行建模，并運用SPIN進(jìn)行自動分析。在信道有誤碼有丟失的情況中，我們分別設(shè)立了兩種錯誤，以進(jìn)一步觀測協(xié)議的運營，分析協(xié)議存在的問題。從而加深對協(xié)議驗證技術(shù)和形式化描述技術(shù)的結(jié)識和理解，進(jìn)一步掌握運用PROMELA語言對協(xié)議進(jìn)行建模，同時掌握SPIN的基本操作，熟悉運用SPIN對網(wǎng)絡(luò)協(xié)議進(jìn)行分析，提高實驗?zāi)芰ΑｊP(guān)鍵詞：模型檢測；AB協(xié)議；SPIN。0.引言隨著計算機通信與網(wǎng)絡(luò)技術(shù)的迅猛發(fā)展，網(wǎng)絡(luò)技術(shù)在人們平常的工作、學(xué)習(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ù)在人們平常的工作、學(xué)習(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及其應(yīng)用。1.1SPIN概述SPIN(SimplePROMELAInterpreter)是一種用丁對并發(fā)系統(tǒng)驗證模型檢測器，采用深度優(yōu)先搜索算法，偏序化簡和on-the-fly策略從不同的角度來解決模型檢測方法中普遍存在的狀態(tài)空間爆炸問題，其適合對協(xié)議驗證。SPIN支持隨機、交互和指導(dǎo)性的自動機驗證，它重要針對設(shè)計規(guī)范進(jìn)行檢測。最早是由貝爾實驗室的形式化方法與驗證小組于1980年開始開發(fā)的。1995年偏序簡約和線性時態(tài)邏輯轉(zhuǎn)換的引入使得SPIN的功能進(jìn)一步擴(kuò)大。2023年推出的SPIN4.0版本支持C代碼的植入，應(yīng)用的靈活性進(jìn)一步增強。隨后2023年推出的SPIN4.1版本加入了深度優(yōu)先搜索算法，2023年連續(xù)推出SPIN5.2版本，這使得SPIN的發(fā)展又上一個新臺階。NASA使用SPIN檢測在1996年火星探測者所存在的錯誤，結(jié)果發(fā)現(xiàn)一些錯誤是可以在發(fā)射之前就可以被檢測并改正的。SPIN從此就被用來檢測土星火箭控制軟件和一些應(yīng)用與外層空間的程序。因SPIN有良好的算法設(shè)計和非凡的檢測能力，得到了ACM(AssociationforComputingMachinery)(世界最早的專業(yè)計算機協(xié)會)的認(rèn)可，在2023年授予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é)；功能強大而簡明的描述系統(tǒng)應(yīng)滿足性質(zhì)屬性規(guī)定的邏輯表達(dá)法：提供一套驗證系統(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描述了SPIN模擬和檢測的過程。PROMELA解析器PROMELA解析器LTL公式解析和轉(zhuǎn)換器SPIN語法錯誤報告驗證機產(chǎn)生器交互模擬模型優(yōu)化測試器執(zhí)行on-the-fly驗證反例圖1-1SPIN模擬和檢測的過程1.2SPIN安裝及使用SPIN可以在很多平臺上運營，具有很多版本，我們在這個實驗中是在Windows764位操作系統(tǒng)中，基于Cygwinlinux模擬器中實現(xiàn)的，下面是簡要的安裝過程。1.軟件準(zhǔn)備：（1）在,withsources版本，最新版本是6.44，下載的文獻(xiàn)名為：spin644.tar.gz。解壓后，里面文獻(xiàn)內(nèi)容：（2）下載并運營cygwin軟件，選擇64位windows版本。選擇默認(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)建桌面和開始菜單文獻(xiàn)，完畢安裝。3）安裝完cygwin后，在系統(tǒng)盤（C盤）會有文獻(xiàn)夾，進(jìn)入：c:/cygwin64/bin中，將第一步已解壓的SPIN文獻(xiàn)夾復(fù)制進(jìn)來，并改名為Spin1。進(jìn)入Spin1文獻(xiàn)夾中的iSpin文獻(xiàn)夾，復(fù)制ispin.tcl至外面的bin目錄中，并去掉.tcl后綴。c.編譯配置ISPIN安裝完cygwin后，先在windows7命令行運營：C:\>setCYGWIN=ttynotitleglob，打開cygwin的控制臺程序：進(jìn)入到spin源碼目錄中c:/cygwin64/bin/spin1/src然后進(jìn)行make：（假如編譯不成功，往往由于cygwin編譯環(huán)境沒裝好，重新檢查安裝環(huán)節(jié)組件的選擇）輸入命令：make–fmakefile成功后，src目錄里會產(chǎn)生spin.exe，將其復(fù)制到bin目錄中。測試tcl環(huán)境(假如找不到相應(yīng)文獻(xiàn)，則無法運營ISPIN，重新檢查安裝環(huán)節(jié)tcl組件的選擇)輸入命令：Whichtclsh輸入命令：Whichwishd.運營ISPIN運營開始->cygwin-x->xwinserver桌面右下角會出現(xiàn)當(dāng)前的xserver的虛擬桌面編號（:2.0）在cygwin的控制臺中指定ISPIN運營界面的虛擬桌面編號輸入命令：exportDISPLAY=:2.0運營ISPIN輸入命令：ispin這樣就可以使用ISPIN。2.實例分析本次實驗重要分析AB協(xié)議，分別針對抱負(fù)狀態(tài)、信道有誤碼無丟失和信道有誤碼有丟失，三種不同的通信環(huán)境，設(shè)計測試三組實驗。在第三組實驗過程中，又進(jìn)行了協(xié)議的兩種錯誤解決。2.1AB協(xié)議簡介AB(AlternatingBit)協(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)的確認(rèn)報文，則重發(fā)該報文；接受端協(xié)議實體在收到報文后，假如確認(rèn)報文無錯誤，并且序號和序號寄存器的值相等，則向發(fā)送端實體發(fā)送確認(rèn)報文(認(rèn)可報文的序號值等于接受報文的序號值)，然后將報文遞交給接受方用戶，序號寄存器的內(nèi)容加l模2。假如接受的報文有錯誤，或者序號不對的，則發(fā)送否認(rèn)確認(rèn)報文。2.2抱負(fù)狀態(tài)下的AB協(xié)議實驗在抱負(fù)狀態(tài)下，信道沒有誤碼，沒有丟失，接受方有無限接受能力。這種狀態(tài)下，協(xié)議比較簡樸，一方發(fā)送，一方接受，不設(shè)超時計時器，不進(jìn)行報文確認(rèn)。下面是協(xié)議的PROMELA描述模型。1#defineMAXSEQ32chanSenderToReceiver=[1]of{int};//只具有1個int類型的通道34proctypeSENDER()//發(fā)送方5{6 intseq=0;7 end: do8 ::SenderToReceiver!seq;//發(fā)送序號9process: seq=(seq+1)%MAXSEQ;//10 od;11 12}1314proctypeRECEIVER()//接受方15{16 intData;17 end1: do18 ::SenderToReceiver?Data;//從通道接受數(shù)據(jù)19 od;20}21//--------------------開始運營協(xié)議-----------------------22init23{24 atomic//原子操作25 {26 runSENDER();27 runRECEIVER();28 }29}將上述代碼保存為RTD1.pml，在ISPIN中打開，點擊SyntaxCheck進(jìn)行語法錯誤檢測，如圖所示，沒有語法錯誤。然后選擇verification選項卡，進(jìn)行模型驗證，模型驗證提成三塊，safety、liveness、以及LTLneverclaims。剛開始我們先對程序進(jìn)行安全性和可活動性驗證，下面截圖中用的是默認(rèn)勾選的選項，第一個表達(dá)死鎖，進(jìn)程無法執(zhí)行下去，第二個表達(dá)程序的斷言沖突（在RTD1.pml中不包含斷言），第三個是允許循環(huán)，就是允許只有一個進(jìn)程一直處在活動狀態(tài)，而另一個不動。點擊run進(jìn)行驗證，如圖所示，沒有存在error。Unreached說明兩個進(jìn)程一直在循環(huán)運營。點擊Simulate/Replay，進(jìn)行模擬重放，點擊(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!Err(8,8)”來分別模擬確認(rèn)報文、否認(rèn)確認(rèn)報文和回執(zhí)報文發(fā)送誤碼三種情況。在SENDER和RECEIVER進(jìn)程中使用了assert語句來檢查在也許會發(fā)生任意的消息丟失的情況下，數(shù)據(jù)是否能所有按順序?qū)Φ牡貍魉偷浇邮芏?。在SENDER和RECEIVER進(jìn)程中使剛progress狀態(tài)標(biāo)記兩端傳送的確的數(shù)據(jù)所必須要執(zhí)行的語句。由于有也許發(fā)送端和接受端只在某些無效的狀態(tài)中循環(huán)，使用progress標(biāo)記可以在檢測過程中檢測出沒有任何實質(zhì)意義的不可推動的循環(huán)。下面是協(xié)議的PROMELA描述模型。1#defineMAXSEQ523mtype={Msg,Ack,Nak,Err};45chanSenderToReceiver=[1]of{mtype,byte,byte};6chanReceiverToSender=[1]of{mtype,byte,byte};78proctypeSENDER(chanInCh,OutCh)9{10byteSendData;//發(fā)送的數(shù)據(jù)11byteSendSeq;//發(fā)送序號12byteReceivedSeq;//接受序號13SendData=MAXSEQ-1;//下一個要發(fā)送的序號14do15 ::SendData=(SendData+1)%MAXSEQ;//下一個消息16again:if17 ::OutCh!Msg(SendData,SendSeq)//對的發(fā)送數(shù)據(jù)18 ::OutCh!Err(8,8)//出現(xiàn)誤碼19fi;2021 if22 ::InCh?Nak(ReceivedSeq,0)->23end: gotoagain//收到否認(rèn)確認(rèn)，重傳24 ::InCh?Err(8,8)->gotoagain//收到ACK誤碼，重傳25 ::InCh?Ack(ReceivedSeq,0)->//收到肯定確認(rèn)26 if2728 ::(ReceivedSeq==SendSeq)->gotoprogress//確認(rèn)號對的，傳下一報文29 ::(ReceivedSeq!=SendSeq)->30end1: gotoagain//確認(rèn)號有誤，重傳31 fi32 fi;33progress: SendSeq=1-SendSeq;//產(chǎn)生下一個報文序號34od;35}3637proctypeRECEIVER(chanInCh,OutCh)38{39byteReceivedData;//接受的數(shù)據(jù)40byteReceivedSeq;//接受的序號41byteExpectedData;//盼望的數(shù)據(jù)42byteExpectedSeq;//盼望的序號4344do45 ::InCh?Msg(ReceivedData,ReceivedSeq)->46 if47 ::(ReceivedSeq==ExpectedSeq)->//數(shù)據(jù)按序到達(dá)，發(fā)送確認(rèn)報文48 assert(ReceivedData==ExpectedData);//檢查數(shù)據(jù)是否能按順序傳送到接受端49progress: ExpectedSeq=1-ExpectedSeq;50 ExpectedData=(ExpectedData+1)%MAXSEQ;51 if52 ::OutCh!Ack(ReceivedSeq,0);//ACK報文對的53 ::OutCh!Err(8,8);//模擬ACK報文誤碼54 ExpectedSeq=1-ExpectedSeq;55 ExpectedData=(ExpectedData+4)%MAXSEQ;56 fi57 58 ::(ReceivedSeq!=ExpectedSeq)->59 if60 ::OutCh!Nak(ReceivedSeq,0);//數(shù)據(jù)不按序到達(dá)，發(fā)送否認(rèn)確認(rèn)報文61 ::OutCh!Err(8,8);//模擬ACK報文誤碼62 fi63 fi64 ::InCh?Err->OutCh!Nak(ReceivedSeq,0);//數(shù)據(jù)錯誤，發(fā)送否認(rèn)確認(rèn)報文65od;66}676869init70{71 atomic//原子操作，執(zhí)行過程不允許打斷72 {73 runSENDER(ReceiverToSender,SenderToReceiver);//發(fā)送者74 runRECEIVER(SenderToReceiver,ReceiverToSender);//接受者75 }76}將上述代碼保存為RTD2.pml，在ISPIN中打開，點擊SyntaxCheck進(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)、對的確認(rèn)、回執(zhí)產(chǎn)生誤碼和發(fā)送報文產(chǎn)生誤碼的情況。否認(rèn)確認(rèn)確認(rèn)報文否認(rèn)確認(rèn)確認(rèn)報文回執(zhí)誤碼發(fā)送誤碼2.4信道有誤碼、有丟失下的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)”和“skip”分別模擬對的傳送、誤碼和丟包三種情況；通過進(jìn)程RECEIVER的發(fā)送語句“OutCh!Ack(ReceivedSeq,0)”、“OutCh!Nak(ReceivedSeq,0)”、“OutCh!Err(8,8)”和“skip”來分別模擬確認(rèn)報文、否認(rèn)確認(rèn)報文、回執(zhí)報文發(fā)送誤碼和回執(zhí)報文丟失三種情況。進(jìn)程RECEIVER中，對對的接受的報文回執(zhí)時，產(chǎn)生回執(zhí)報文誤碼“OutCh!Err(8,8)”和丟包“skip”的情況，應(yīng)當(dā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ù)是否能所有按順序?qū)Φ牡貍魉偷浇邮芏?。在SENDER和RECEIVER進(jìn)程中使剛progress狀態(tài)標(biāo)記兩端傳送的確的數(shù)據(jù)所必須要執(zhí)行的語句。由于有也許發(fā)送端和接受端只在某些無效的狀態(tài)中循環(huán)，使用progress標(biāo)記可以在檢測過程中檢測出沒有任何實質(zhì)意義的不可推動的循環(huán)。在此實驗中，我們分別模擬了兩種錯誤情況：一是發(fā)送方對否認(rèn)確認(rèn)報文的忽略，二是接受方在回執(zhí)發(fā)生丟包時，未及時還原盼望接受數(shù)據(jù)和盼望接受序號。下面是協(xié)議的PROMELA描述模型。1#defineMAXSEQ523mtype={Msg,Ack,Nak,Err};45chanSenderToReceiver=[1]of{mtype,byte,byte};6chanReceiverToSender=[1]of{mtype,byte,byte};78proctypeSENDER(chanInCh,OutCh)9{10byteSendData;//發(fā)送的數(shù)據(jù)11byteSendSeq;//發(fā)送序號12byteReceivedSeq;//接受序號13SendData=MAXSEQ-1;//下一個要發(fā)送的序號14do15 ::SendData=(SendData+1)%MAXSEQ;//下一個消息16again:if17 ::OutCh!Msg(SendData,SendSeq)//對的發(fā)送數(shù)據(jù)18 ::OutCh!Err(8,8)//出現(xiàn)誤碼19 ::skip//報文丟失20fi;2122 if23 ::timeout->gotoagain//超時重傳24 ::InCh?Nak(ReceivedSeq,0)->25end: gotoagain//收到否認(rèn)確認(rèn)，重傳26 ::InCh?Err(8,8)->gotoagain//收到ACK誤碼，重傳27 ::InCh?Ack(ReceivedSeq,0)->//收到肯定確認(rèn)28 if2930 ::(ReceivedSeq==SendSeq)->gotoprogress//確認(rèn)號對的，傳下一報文31 ::(ReceivedSeq!=SendSeq)->32end1: gotoagain//確認(rèn)號有誤，重傳33 fi34 fi;35progress: SendSeq=1-SendSeq;//產(chǎn)生下一個報文序號36od;37}3839proctypeRECEIVER(chanInCh,OutCh)40{41byteReceivedData;//接受的數(shù)據(jù)42byteReceivedSeq;//接受的序號43byteExpectedData;//盼望的數(shù)據(jù)44byteExpectedSeq;//盼望的序號4546do47 ::InCh?Msg(ReceivedData,ReceivedSeq)->48 if49 ::(ReceivedSeq==ExpectedSeq)->//數(shù)據(jù)按序到達(dá)，發(fā)送確認(rèn)報文50 assert(ReceivedData==ExpectedData);//檢查數(shù)據(jù)是否能按順序傳送到接受端51progress: ExpectedSeq=1-ExpectedSeq;52 ExpectedData=(ExpectedData+1)%MAXSEQ;53 if54 ::OutCh!Ack(ReceivedSeq,0);//ACK報文對的55 ::OutCh!Err(8,8);//模擬ACK報文誤碼，并還原盼望的序號和數(shù)據(jù)56 ExpectedSeq=1-ExpectedSeq;57 ExpectedData=(ExpectedData+4)%MAXSEQ;58 ::skip//報文丟失，并還原盼望的序號和數(shù)據(jù)59 ExpectedSeq=1-ExpectedSeq;60 ExpectedData=(ExpectedData+4)%MAXSEQ;61 fi62 63 ::(ReceivedSeq!=ExpectedSeq)->64 if65 ::OutCh!Nak(ReceivedSeq,0);//數(shù)據(jù)不按序到達(dá)，發(fā)送否認(rèn)確認(rèn)報文66 ::OutCh!Err(8,8);//模擬ACK報文誤碼67 ::skip//報文丟失68 fi69 fi70 ::InCh?Err(8,8)->OutCh!Nak(ReceivedSeq,0);//數(shù)據(jù)錯誤，發(fā)送否認(rèn)確認(rèn)報文71od;72}737475init76{77 atomic//原子操作，執(zhí)行過程不允許打斷78 {79 runSENDER(ReceiverToSender,SenderToReceiver);//發(fā)送者80 runRECEIVER(SenderToReceiver,ReceiverToSender);//接受者81 }82}將上述代碼保存為RTD3.pml，在ISPIN中打開，點擊SyntaxCheck進(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)、對的確認(rèn)、回執(zhí)產(chǎn)生誤碼和發(fā)送報文產(chǎn)生誤碼的情況。丟包回執(zhí)誤碼丟包回執(zhí)誤碼發(fā)送誤碼對的確認(rèn)否認(rèn)確認(rèn)2.4.1下面來觀測兩種錯誤的解決。1.發(fā)送方對否認(rèn)確認(rèn)報文的忽視假如我們修改25行中，對否認(rèn)確認(rèn)報文對的的解決應(yīng)當(dāng)是重傳，而改為忽視，不重傳，還是繼續(xù)發(fā)送下一個數(shù)據(jù)，則在進(jìn)行模型驗證時，會產(chǎn)生一個錯誤“assertionviolated(ReceivedData==ExpectedData)(atdepth121)”，我們在程序中第50行用assert標(biāo)記進(jìn)行檢查數(shù)據(jù)是否能按順序傳送到接受端時，系統(tǒng)產(chǎn)生違反這一檢測的錯誤。在進(jìn)行Simulate/Replay，進(jìn)行模擬重放，在Mode選項頁中，會自動勾選Guided，withtrail，ISPIN會將錯誤的運營結(jié)果存儲到RTD3.pml.trail文獻(xiàn)中，點擊(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對于接受者REC