网络协议工程实验报告

1、网络协议工程实验报告一.题目描述1 .将6.3节描述的协议条件吗改为：报文和应答均会出错，且都丢失，接收方没有无限能力，这就是我们通常所说的使用的停等协议。请用PROMELA进行描述，并用SPIN模拟运行，一般性验证，无进展循环验证和认为假如错误进行验证。2 .请根据图6-16写出著名的AB协议的PROMELA描述，并验证“A获取的每一个报文至少一次是正确的，而B接收的每一个报文至多有一次是正确的(EverymessagesfetchedbyAisreceivederror-freeatleastonceandacceptedatmostoncebyB)”。二.安装环境安装spin之前先要安装

2、dev-cpp并配置好系统环境变量。此外，还需要安装ActiveTcl85111295590-win32-ix86-threaded.exe,我们所用的有窗口界面的xspin430.tcl需要用到tcl8.5。下载pc_spin430.zip文件，解压pc_spin430.zip然后将spin.exe拷贝到例如d:spin下，安装完后还需要配置系统环境变量，主要是添加gcc的目录。一.分析停止等待协议报文和应答均会出错，丢失，接收方没有无限接收能力。我们用简单的停等协议来解决数据的可靠传输问题，协议主要过程为：发送方发送报文，等待应答，如果是肯定应答则发送下一帧，如果是否定应答或者应答帧出错则

3、重发；接收方接收报文，如果是期望的报文则发送肯定应答，否则发送否设应答，给报文加序号。我们将此协议称为RTD4.0。在RTD3.0的基础上，在mtype=Msg,Ack,Nak,Err,Mis;中添加Mis来模拟报文丢失的情况。在发送端通过InCh?Mis(0,0)来模拟发送报文丢失，在接收端通过InCh?Mis(0,0)模拟应答报文丢失。如果报文丢失，则需要重发报文。AB协议AB(AlternatingBit)协议是最早的端到端通信协议之一。在AB协议系统中，包含有发送端和接受端两个实体。发送端协议实体从发送方获取一个报文，将序号寄存器值赋给报文，然后向接收端实体发出报文，发送方发出报文之后

4、启动超时时钟，等待认可报文。如果在给定的时间内没有收到认可报文，则重发该报文。如果收到认可报文，其序号与发出报文序号相同，则序号寄存器的内容加1模2,然后发送端实体从发送方用户获取下一个报文；接收端协议实体在收到报文后，如果确认报文无错误，并且序号和序号寄存器的值相等，则向发送端实体发送认可报文(认可报文的序号值等于接收报文的序号值)，然后将报文递交给接收方用户，序号寄存器的内容加1模2。如果接收的报文有错误，或者序号不正确，则丢失报文。四.实验程序停止等待协议：#defineMAXSEQ5mtype=Msg,Ack,Nak,Err,Miss;chanSenderToReceiver=1ofm

5、type,byte,byte;chanReceiverToSender=1ofmtype,byte,byte;proctype SENDER(chan InCh,OutCh) byte SendData;byte SendSeq;byte ReceivedSeq;SendData=MAXSEQ-1; do/* 发送的数据*/* 发送序号*/*接收到的报文序号*/again:SendData=(SendData+1)%MAXSEQ; if:OutCh!Msg(SendData,SendSeq):OutCh!Err(0,0):OutCh!Miss(0,0)fi;/* 正常发送数据*/* 模拟出现无

6、码*/* 模拟丢失*/ifend1:timeout -> goto again :InCh?Miss(0,0) ->goto again:InCh?Err(0,0)->goto again:InCh?Nak(ReceivedSeq,0)-> goto again:InCh?Ack(ReceivedSeq,0)->if/* 模仿ack 丢失，重发报文*/* 收到ack 误码，重发报文*/*收到否定确认，重发报文*/*受到肯定应答，且序号正确发送下一个报文*/:(ReceivedSeq=SendSeq)->gotoprogress:(ReceivedSeq!=S

7、endSeq)->end2:发前一个报文goto again/*受到肯定应答，但序号不正确，重*/fifi;progress: od;SendSeq=1-SendSeq;/* 产生下一个报文的发送序列*/proctypeRECEIVER(chanInCh,OutCh)byte ReceivedData;byte ReceivedSeq;byte ExpectedData;byte ExpectedSeq;do/* 接收到的报文数据*/* 接收到的报文序号*/* 期望收到的报文数据*/* 期望收到的报文序号*/* 接收到正常的报文*/* 报文按序到达，发送肯定确认:InCh?Msg(Rec

8、eivedData,ReceivedSeq)->if:(ReceivedSeq=ExpectedSeq)->*/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出现误码*/ExpectedSeq=1-ExpectedSeq;ExpectedData=(Expecte

9、dData+4)%MAXSEQ;fi:(ReceivedSeq!=ExpectedSeq)->if:OutCh!Nak(ReceivedSeq,0);/*报文失序到达，发送否定确认*/:OutCh!Err(0,0);/*模拟nak出现无码*/fifi:InCh?Err(0,0)->OutCh!Nak(ReceivedSeq,0);/*接收到有误码的报文*/:InCh?Miss(0,0)->skip;od;initrunSENDER(ReceiverToSender,SenderToReceiver);runRECEIVER(SenderToReceiver,ReceiverT

10、oSender);AB协议mtype=a,b,err;chanAtoB=1ofmtype,byte;chanBtoA=1ofmtype,byte;proctypeA(chanInCh,OutCh)s5:if:OutCh!a(0);gotos4;:OutCh!err(0);fi;s4:if:InCh?err(0)->gotos5;:InCh?b(0)->gotos1;:InCh?b(1)->gotos1;fi;s1:if:OutCh!a(1);:OutCh!err(0);fi;gotos2;52:if:InCh?err(0);gotos5;:InCh?b(1);gotos1;:

11、InCh?b(0);gotos3;fi;53: InCh?a(1);gotos2;proctypeB(chanInCh,OutCh)54: if:InCh?err(0);gotos5;:InCh?a(0);gotos1;:InCh?a(1);gotos1;fi;51: if:OutCh!b(1);:OutCh!err(0);fi;gotos2;52: if:InCh?err(0);gotos5;:InCh?a(0);gotos3;:InCh?a(1);gotos1;fi;53: if:OutCh!b(1);:OutCh!err(0);fi;gotos2;s5:if:OutCh!b(0);:Ou

12、tCh!err(0);fi;gotos4;initatomicrunA(AtoB,BtoA);runB(BtoA,AtoB);五运行结果停止等待协议：模拟运行：irrSY£in；EEQp"白依#"Pr-#fY#般性验证:VerificationOutputI?I回Searchfor:Find二(SpinVersion4,3Q22June2U07)+PartialOrderReductionFullstatespacesearchfor:neverclaim-trotsel&cted)assertionviolations-(disabledby-Aflag

13、)cydechecks-(disabledby-DSAFETY)invalidendstates+State-vector46bte.depthreached1C&.errors04114states,stored121states,matched536transit!ons(-stored+matched)0atomicslepshashconflicts:0(resolved)Statsanmernoryusage(inMegabyte动：0.023equivalentmernoryusageforslates(sloredT(State-vector+oveftieadj)0.3

14、01actualmemor)usageforstates(.unsuccessfulcompression:1298.14%)State-vedorasstored-719hyte*Sbyteoverhead2097memoryusedfoihashtable0.220memoryusedforDFSstack(-nrlODOO)0,096memoryIosttofragmentation2,G22totalactualrnernoryusag&unreachedinproctypeSENDERli依犯,“白n_irfr2恰忸31/-end-11(itof31states)unreac

15、hedinproctypeRECEl'/ERline59,"panjn",state27,"-end-flaf27states)unreacriedinproctypeinit:(0of3slates)Savein;C:/U5eir5摩ClearClc&e无进展循环验证:YeriHcatorQi.tputSearchfor:Findpan:non-wQwesscycle(atdeptti8)pan：wQtepan-in.trail(SpinVersion4.3.0-22Jun&2007)Warning:Searctinotcompleted

16、+PartialOrderReductionFullstatespacesearchfar:neverclaim+assertionviolations+(ifwithinscopeofclaim)non-progresscydes+(fairnessdisabled)invalidendstates-(disabledbyneverdaimlState-7edor52byte,depthreadied17,errors:112states,stored(15,isited)1slates,matched16transitions(-wlsited+matchedOatoiTiicstep5h

17、ashconflicts：0(resolved)Statsonmemory曰g建(in蒯ega。/忸韵:0001equivalentmemor),usageforslates(5loe(T(St3m-¥Ecto+overhead)03fl1actualmemoryusageforslates(.unsuccessfulcompression:39187.50%>State-Fedorassiored=2606Sbyte+12byteoverhead2097memoryusedforhashtable0.320memoryusedforDFSstscK(-mlOOOO)0,09B

18、memoryIoattoTtagmentation2&ZtotalactualmernousageunreachedinproctypeSENDERline3&,state27,SendSeq=(1-SendSeqfline38.',pan_instateSl."-end-"(2of31states)unreach&dinproctypGRECEl/ERlift白52."pan_in;state5,"Exped&dData=(ExperfedData+1)%5fline57,"pan_in",state9."ExpededSeq=dpectedSeqlline53h"panlinstateH.XfutChSMisOfifiB53."