網(wǎng)絡(luò)協(xié)議工程.doc

網(wǎng)絡(luò)協(xié)議工程實驗報告一 題目描述1. 將6.3節(jié)描述的協(xié)議條件嗎改為：報文和應(yīng)答均會出錯，且都丟失，接收方?jīng)]有無限能力，這就是我們通常所說的使用的停等協(xié)議。請用PROMELA進(jìn)行描述，并用SPIN模擬運行，一般性驗證，無進(jìn)展循環(huán)驗證和認(rèn)為假如錯誤進(jìn)行驗證。2. 請根據(jù)圖6-16寫出著名的AB協(xié)議的PROMELA描述，并驗證“A獲取的每一個報文至少一次是正確的，而B接收的每一個報文至多有一次是正確的（Every messages fetched by A is received error-free at least once and accepted at most once by B）”。二安裝環(huán)境安裝spin之前先要安裝dev-cpp并配置好系統(tǒng)環(huán)境變量。此外，還需要安裝ActiveTcl8.5.11.1.295590-win32-ix86-threaded.exe，我們所用的有窗口界面的xspin430.tcl需要用到tcl8.5。下載pc_spin430.zip文件，解壓pc_spin430.zip然后將spin.exe拷貝到例如d: spin下，安裝完后還需要配置系統(tǒng)環(huán)境變量，主要是添加gcc的目錄。一. 分析停止等待協(xié)議報文和應(yīng)答均會出錯，丟失，接收方?jīng)]有無限接收能力。我們用簡單的停等協(xié)議來解決數(shù)據(jù)的可靠傳輸問題，協(xié)議主要過程為：發(fā)送方發(fā)送報文，等待應(yīng)答，如果是肯定應(yīng)答則發(fā)送下一幀，如果是否定應(yīng)答或者應(yīng)答幀出錯則重發(fā)；接收方接收報文，如果是期望的報文則發(fā)送肯定應(yīng)答，否則發(fā)送否設(shè)應(yīng)答，給報文加序號。我們將此協(xié)議稱為RTD4.0。在RTD3.0的基礎(chǔ)上，在mtype = Msg, Ack, Nak, Err, Mis;中添加Mis來模擬報文丟失的情況。在發(fā)送端通過InCh?Mis(0,0)來模擬發(fā)送報文丟失，在接收端通過InCh?Mis(0,0)模擬應(yīng)答報文丟失。如果報文丟失，則需要重發(fā)報文。AB協(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)容加1模2，然后發(fā)送端實體從發(fā)送方用戶獲取下一個報文；接收端協(xié)議實體在收到報文后，如果確認(rèn)報文無錯誤，并且序號和序號寄存器的值相等，則向發(fā)送端實體發(fā)送認(rèn)可報文（認(rèn)可報文的序號值等于接收報文的序號值），然后將報文遞交給接收方用戶，序號寄存器的內(nèi)容加1模2。如果接收的報文有錯誤，或者序號不正確，則丟失報文。四實驗程序 停止等待協(xié)議：#define MAXSEQ 5mtype=Msg,Ack,Nak,Err,Miss;chan SenderToReceiver=1ofmtype,byte,byte;chan ReceiverToSender=1ofmtype,byte,byte;proctype SENDER(chan InCh,OutCh)byte SendData; /*發(fā)送的數(shù)據(jù)*/byte SendSeq; /*發(fā)送序號*/byte ReceivedSeq; /*接收到的報文序號*/SendData=MAXSEQ-1;do :SendData=(SendData+1)%MAXSEQ;again:if :OutCh!Msg(SendData,SendSeq) /*正常發(fā)送數(shù)據(jù)*/ :OutCh!Err(0,0) /*模擬出現(xiàn)無碼*/ :OutCh!Miss(0,0) /*模擬丟失*/ fi;if :timeout - goto again :InCh?Miss(0,0) -goto again /*模仿ack丟失，重發(fā)報文*/ :InCh?Err(0,0)-goto again /*收到ack誤碼，重發(fā)報文*/ :InCh?Nak(ReceivedSeq,0)- /*收到否定確認(rèn)，重發(fā)報文*/ end1:goto again :InCh?Ack(ReceivedSeq,0)-if /*受到肯定應(yīng)答，且序號正確發(fā)送下一個報文*/ :(ReceivedSeq=SendSeq)-goto progress :(ReceivedSeq!=SendSeq)-end2:goto again /*受到肯定應(yīng)答，但序號不正確，重發(fā)前一個報文*/fifi;progress:SendSeq=1-SendSeq; /*產(chǎn)生下一個報文的發(fā)送序列*/od;proctype RECEIVER(chan InCh,OutCh)byte ReceivedData; /*接收到的報文數(shù)據(jù)*/byte ReceivedSeq; /*接收到的報文序號*/ byte ExpectedData; /*期望收到的報文數(shù)據(jù)*/byte ExpectedSeq; /*期望收到的報文序號*/do :InCh?Msg(ReceivedData,ReceivedSeq)- /*接收到正常的報文*/ if:(ReceivedSeq=ExpectedSeq)- /*報文按序到達(dá)，發(fā)送肯定確認(rèn)*/assert(ReceivedData=ExpectedData);progress:ExpectedSeq=1-ExpectedSeq;ExpectedData=(ExpectedData+1)%MAXSEQ;if :OutCh!Miss(0,0); /*模擬ack丟失*/ :OutCh!Ack(ReceivedSeq,0); :OutCh!Err(0,0); /*模擬ack出現(xiàn)誤碼*/ExpectedSeq=1-ExpectedSeq;ExpectedData=(ExpectedData+4)%MAXSEQ;fi:(ReceivedSeq!=ExpectedSeq)-if :OutCh!Nak(ReceivedSeq,0); /*報文失序到達(dá)，發(fā)送否定確認(rèn)*/ :OutCh!Err(0,0); /*模擬nak出現(xiàn)無碼*/ fifi:InCh?Err(0,0)-OutCh!Nak(ReceivedSeq,0); /*接收到有誤碼的報文*/:InCh?Miss(0,0) -skip; od;initrun SENDER(ReceiverToSender,SenderToReceiver);run RECEIVER(SenderToReceiver,ReceiverToSender);AB協(xié)議mtype=a,b,err;chan AtoB=1ofmtype,byte;chan BtoA=1ofmtype,byte;proctype A(chan InCh,OutCh)s5: if :OutCh!a(0); goto s4; :OutCh!err(0); fi;s4: if:InCh?err(0)-goto s5;:InCh?b(0)-goto s1;:InCh?b(1)-goto s1; fi;s1: if:OutCh!a(1);:OutCh!err(0);fi;goto s2;s2: if:InCh?err(0);goto s5;:InCh?b(1);goto s1;:InCh?b(0);goto s3;fi;s3: InCh?a(1);goto s2;proctype B(chan InCh,OutCh)s4:if :InCh?err(0);goto s5; :InCh?a(0);goto s1; :InCh?a(1);goto s1; fi;s1:if:OutCh!b(1);:OutCh!err(0);fi;goto s2;s2:if :InCh?err(0);goto s5; :InCh?a(0);goto s3; :InCh?a(1);goto s1;