网络协议工程

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

2、.安装环境安装spin之前先要安装dev-cpp并配置好系统环境变量。此外，还需要安装ActiveTcl8.5.11.1.295590-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 (Alternating Bit )协议是最早的端到端通信协议之一。在AB协议系统中，包含有发送端和接受端两个实体。发送端协议实体从发送方获取一个报文，

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

5、k,Nak,Err,Miss;cha n Sen derToReceiver=1ofmtype,byte,byte;cha n ReceiverToSe nder=1ofmtype,byte,byte;proctype SENDER(cha n In Ch,OutCh)byte SendData;/* 发送的数据 */byte SendSeq;/* 发送序号 */en d1:timeout - goto aga in:I nCh?Miss(0,0) -goto agai n:I nCh?Err(0,0)-goto again:I nCh?Nak(ReceivedSeq,O)- goto aga

6、 in:I nCh?Ack(ReceivedSeq,O)- if/*模仿ack丢失，重发报文*/*收到ack误码，重发报文*/*收到否定确认，重发报文*/byte ReceivedSeq;/*接收到的报文序号Sen dData=MAXSEQ-1;do*/aga in:Se ndData=(Se ndData+1)%MAXSEQ; if:OutCh!Msg(Se ndData,Se ndSeq):OutCh!Err(0,0):OutCh!Miss(O,O)fi;if/*正常发送数据*/*模拟出现无码*/*模拟丢失*/en d2:发前一个报文*/fi/*受到肯定应答，且序号正确发送下一个报文:(R

7、eceivedSeq=Se ndSeq)-goto progress :(ReceivedSeq!=Se ndSeq)-goto aga in*/*受到肯定应答，但序号不正确，重fi;progress:od;proctype RECEIVER(chan In Ch,OutCh)byte ReceivedData;byte ReceivedSeq;byte ExpectedData;byte ExpectedSeq;do:I nCh?Msg(ReceivedData,ReceivedSeq)- ifSen dSeq=1-Se ndSeq;/*产生下一个报文的发送序列*/*接收到的报文数据*/*接

8、收到的报文序号*/*期望收到的报文数据/*期望收到的报文序号*/*/*接收到正常的报文*/progress:(ReceivedSeq=ExpectedSeq)-/*报文按序到达，发送肯定确认assert(ReceivedData=ExpectedData);ExpectedSeq=1-ExpectedSeq;ExpectedData=(ExpectedData+1)%MAXSEQ; if:OutCh!Miss(0,0);/*模拟 ack 丢失 */:OutCh!Ack(ReceivedSeq,O);*/:OutCh!Err(0,0);/*模拟 ack 出现误码 */ExpectedSeq=1-

9、ExpectedSeq;ExpectedData=(ExpectedData+4)%MAXSEQ;fi:(ReceivedSeq!=ExpectedSeq)-if:OutCh!Nak(ReceivedSeq,0);/*报文失序到达，发送否定确认*/:OutCh!Err(0,0);/*模拟 nak 出现无码 */fifi:l nCh?Err(0,0)-OutCh!Nak(ReceivedSeq,0);/* 接收到有误码的报文 */:l nCh?Miss(O,O) -skip;od;initrun SENDER(ReceiverToSe nder,Se nderToReceiver);run RE

10、CEIVER(Se nderToReceiver,ReceiverToSe nder);AB协议mtype=a,b,err;chan AtoB=1ofmtype,byte;chan BtoA=1ofmtype,byte;proctype A(chanIn Ch,OutCh)s5:if:OutCh!a(0); goto s4;:OutCh!err(0);fi;s4:if:I nCh?err(0)-goto s5;:I nCh?b(0)-goto s1;:I nCh?b(1)-goto s1; fi;s1:if:OutCh!a(1); :OutCh!err(0); fi;goto s2;s2:if

11、:I nCh?err(0);goto s5;:I nCh?b(1);goto s1;:l nCh?b(0);goto s3;fi;s3:In Ch?a(1); goto s2;proctype B(chan In Ch,OutCh)s4:if:I nCh?err(0);goto s5;:I nCh?a(0);goto s1;:InCh?a(1);goto s1; fi;s1:if:OutCh!b(1); :OutCh!err(O); fi;goto s2;s2:if:I nCh?err(0);goto s5;:I nCh?a(0);goto s3;:InCh?a(1);goto s1; fi;

12、s3:if:OutCh!b(1); :OutCh!err(0); fi;goto s2;s5:if:OutCh!b(0); :OutCh!err(0); fi;goto s4; initatomicrun A(AtoB,BtoA); run B(BtoA,AtoB); 五.运行结果 停止等待协议: 模拟运行：S8PrsrY般性验证納 Secuence ChartSwu in; mw叭13a21 123 I,02830回Search fo2 097 0 220 O.OS0 2.22Verificat on Output(Spin Version 4 3 022 June 2007)+ Parti

13、al Order Reductionequivalent mernof)usage for slates (storedT(State-vector + oveftieadj) actual memor)usage for states (.unsuccessful compression: 1298.14%) State-vedoras stored - 719 Byte 十 S ftyte overhead memory usedfor hash tabl (-w19 memory usedforLTE stack (-nrlODOOjme mor/ lost to fragmentati

14、ontotal actual memory usag&State sector 46 byte, depth reached 108, errors: 0 414 states, stored121 states, matched535 transitions (二 stored+matched 0 atomiGste pshash conflicts： o (resolved)Full stale space search for:never claim -(not seiscted) assertion violations - (disabled by -A flag) cycl e c

15、hecks - (disb led by -DSAFETY invalid nd states +Stats an mernory usage in Megab/&s) 0 0230.301unreached in prodypeSEMDER lint 38, *panjn, state 31, -&nd- (1 of 31 statesunrea匚hmd in proclype RECEI /ER line 69. paiUn； state 27,w-end- (1 af 27 states)unreacrisd in proctype init:(0 ofSsiates)gave in:?

16、:/Users尽律 ClearCloseL无进展循环验证pan: non-progress cycle (at deptti 8)pan： wrote pn,trail(Spin Version 4.3.0 -22June 2007)Warning: Searcti not completed+ Partial Order ReductionFull state space search far:never daim +assertion violations + 肃训ittiin scope of Glairn) non-progress cycles + (fairness disable

17、d) invalid end states -disabled by never daim) Veriicat on OutputSearch for:ave in: Ci/Users/sKj? ClearStat&-7edor 52 byte, depth readied 17, errors: 112 states, stored (15 ,isited)1 slates, nnatctied16 transttions (- sited*matched OatoiTiicstephash conflicts： 0 (resolved)Stats on memory (in0 001 eq

18、uivalent memor)usage for slates (slo re (instate-vector 十 overt! ead)0 301 actual memory usage for slates (.unsuccessful compression: 39187.50%) State-Fedoras sioretl = 2606S byte + 12 byte overhead2 097 memory usedfor hash table (-w19)0.320 memory usedforDFS stsclc(-mlOOOO)memory Io at to Ttagmentation2.22 total actual merno usageunreached in proctpe SE ND ERline 35. pan_inr state 27,SendSeq = (1 -SendSeqfline 38. pan_ln,l stale 31r-Bn(t*(2 of 31 states)unreach&d in proctyp&RECEl /ERH fie 52. pan_in? state 5. Exped&dData 二(ExperfedData+1 )%5f line 57,pan,_in, state 9. E