1、網絡協議工程SPIN實驗報告摘要：本文主要介紹了一種基于模型檢測的協議自動分析工具SPIN的使用。對經典的AB協議在理想狀態、信道有誤碼無丟失和信道有誤碼有丟失三種不同環境中分別進行建模，并運用SPIN進行自動分析。在信道有誤碼有丟失的情況中，我們分別設置了兩種錯誤，以進一步觀察協議的運行，分析協議存在的問題。從而加深對協議驗證技術和形式化描述技術的認識和理解，進一步掌握運用PROMELA語言對協議進行建模，同時掌握SPIN的基本操作，熟悉運用SPIN對網絡協議進行分析，提高實驗能力。關鍵詞：模型檢測；AB協議；SPIN。0.引言隨著計算機通信與網絡技術的迅猛發展，網絡技術在人們日常的工作、學

2、習和生活的各個方面都得到了普遍地運用。各種網絡通信系統在提供越來越豐富的功能的同時，其設計和實現也日益復雜。面對復雜網絡系統的挑戰，傳統的自然語言進行的協議描述，雖然具有表達能力強、可讀性好、方便的優點，但是存在不嚴格、不精確、沒有描述標準和存有二義性等缺點。形式化方法使得對網絡通信系統的描述、實現和測試變得容易，在對于協議實現、測試的自動化和協議驗證上得到了廣泛運用。本文主要介紹一種基于模型檢測的協議自動分析工具SPIN及其在分析網絡協議中的應用。1.SPIN概述隨著計算機通信與網絡技術的迅猛發展，網絡技術在人們日常的工作、學習和生活的各個方面都得到了普遍運用。各種網絡通信系統在提供越來越豐

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

20、gt; /數據按序到達，發送確認報文48assert(ReceivedData=ExpectedData); /檢驗數據是否能按順序傳送到接收端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); /數據不按序到達，發送否定確認報文61:OutCh!Err(8,8); /模擬ACK報文誤碼62fi63fi64:InCh?Err -> OutCh!Nak(ReceivedSeq,0); /數據錯誤，發送否定確認報文65 od;66 676869 init70 71atomic /原子操作，執行過程不允許打斷7273run SENDER(ReceiverToSender,SenderToReceiver);/發送者74run RECEIVER(SenderToRec

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

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

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

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

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

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

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

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

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

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

33、統產生違反這一檢測的錯誤。在進行Simulate/Replay，進行模擬重放，在Mode選項頁中，會自動勾選Guided，with trail，ISPIN會將錯誤的運行結果存儲到RTD3.pml.trail文件中，點擊(Re)Run進行回放，在運行到最后一步時，我們從變量窗口發現：RECEIVER(2):ExpectedData = 0RECEIVER(2):ExpectedSeq = 0RECEIVER(2):ReceivedData = 2RECEIVER(2):ReceivedSeq = 0SENDER(1):ReceivedSeq = 1SENDER(1):SendData = 2SENDER(1):SendSeq = 0對于接收者RECEIVER（）來說，期望接收到的數據是0，但是實際接收到的數據為2，