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

1、歡迎下載內(nèi)容僅供參考網(wǎng)絡(luò)協(xié)議工程實(shí)驗(yàn)報(bào)告一 題目描述將 6.3 節(jié)描述的協(xié)議條件嗎改為：報(bào)文和應(yīng)答均會(huì)出錯(cuò)，且都丟失，接收方?jīng)]有無(wú)限能PROMELASPIN一般性驗(yàn)證，無(wú)進(jìn)展循環(huán)驗(yàn)證和認(rèn)為假如錯(cuò)誤進(jìn)行驗(yàn)證。請(qǐng)根據(jù)圖6-16寫(xiě)出著名的AB協(xié)議的PROMELA描述，并驗(yàn)證獲取的每一個(gè)報(bào)文至少一次是正確的，而B(niǎo)messages fetched by is received error-free at least once and accepted at most once by 二安裝環(huán)境spindev-cpp 需要用到tcl8.5。下載pc_spin430.zip 文件，解壓pc_spin430.

2、zip 拷貝到例如d: spingcc目錄。一. 分析停止等待協(xié)議RTD4.0。在RTD3.0 的基礎(chǔ)上，在mtype = Msg, Ack, Nak, Err, Mis送端通過(guò)InCh?Mis(0,0)來(lái)模擬發(fā)送報(bào)文丟失，在接收端通過(guò)InCh?Mis(0,0)模擬應(yīng)答報(bào)文丟失。如果報(bào)文丟失，則需要重發(fā)報(bào)文。AB 協(xié)議AB（Alternating Bit）協(xié)議是最早的端到端通信協(xié)議之一。在AB12，然后發(fā)送端實(shí)體從發(fā)送方用戶(hù)獲取下一個(gè)報(bào)文；接收端協(xié)實(shí)體發(fā)送認(rèn)可報(bào)文（認(rèn)可報(bào)文的序號(hào)值等于接收?qǐng)?bào)文的序號(hào)值，然后將報(bào)文遞交給接收方用1。如果接收的報(bào)文有錯(cuò)誤，或者序號(hào)不正確，則丟失報(bào)文。四實(shí)驗(yàn)程序停止

3、等待協(xié)議： #define MAXSEQ mtype=Msg,Ack,Nak,Err,Miss;chan SenderToReceiver=1ofmtype,byte,byte; chan ReceiverToSender=1ofmtype,byte,byte;proctype SENDER(chan InCh,OutCh)byte SendData;*/byte SendSeq;*/byte ReceivedSeq;SendData=MAXSEQ-1;do:SendData=(SendData+1)%MAXSEQ; again:if:OutCh!Msg(SendData,SendSeq)*/

4、:OutCh!Err(0,0)*/:OutCh!Miss(0,0)*/fi;if:timeout - goto again:InCh?Miss(0,0) -goto againack*/:InCh?Err(0,0)-goto againack*/:InCh?Nak(ReceivedSeq,0)-收到否定確認(rèn)，重發(fā)報(bào)end1:goto again:InCh?Ack(ReceivedSeq,0)- if/*受到肯定應(yīng)答，且序號(hào)正確發(fā)送下一個(gè)報(bào)文*/:(ReceivedSeq=SendSeq)-goto progress:(ReceivedSeq!=SendSeq)-end2:goto again*

5、/fifi;progress:SendSeq=1-SendSeq;od;proctype RECEIVER(chan InCh,OutCh)byte ReceivedData;*/byte ReceivedSeq;*/byte ExpectedData;*/byte ExpectedSeq;do:InCh?Msg(ReceivedData,ReceivedSeq)-if:(ReceivedSeq=ExpectedSeq)-認(rèn)*/assert(ReceivedData=ExpectedData); progress:ExpectedSeq=1-ExpectedSeq;ExpectedData=(

6、ExpectedData+1)%MAXSEQ; if:OutCh!Miss(0,0);ack*/:OutCh!Ack(ReceivedSeq,0);:OutCh!Err(0,0);ackExpectedSeq=1-ExpectedSeq; ExpectedData=(ExpectedData+4)%MAXSEQ;定確認(rèn)*/fi:(ReceivedSeq!=ExpectedSeq)- if:OutCh!Nak(ReceivedSeq,0);:OutCh!Err(0,0);nakfifi:InCh?Err(0,0)-OutCh!Nak(ReceivedSeq,0);*/:InCh?Miss(0,0

7、)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(chanInCh,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)-got

8、o s1;fi;s1:iffi;:OutCh!a(1);:OutCh!err(0);s2:goto 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; fi;s3:if:OutCh!