网络协议工程.doc

网络协议工程实验报告一 题目描述1. 将6.3节描述的协议条件吗改为：报文和应答均会出错，且都丢失，接收方没有无限能力，这就是我们通常所说的使用的停等协议。请用PROMELA进行描述，并用SPIN模拟运行，一般性验证，无进展循环验证和认为假如错误进行验证。2. 请根据图6-16写出著名的AB协议的PROMELA描述，并验证“A获取的每一个报文至少一次是正确的，而B接收的每一个报文至多有一次是正确的（Every messages fetched by A is received error-free at least once and accepted at most once by B）”。二安装环境安装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的目录。一. 分析停止等待协议报文和应答均会出错，丢失，接收方没有无限接收能力。我们用简单的停等协议来解决数据的可靠传输问题，协议主要过程为：发送方发送报文，等待应答，如果是肯定应答则发送下一帧，如果是否定应答或者应答帧出错则重发；接收方接收报文，如果是期望的报文则发送肯定应答，否则发送否设应答，给报文加序号。我们将此协议称为RTD4.0。在RTD3.0的基础上，在mtype = Msg, Ack, Nak, Err, Mis;中添加Mis来模拟报文丢失的情况。在发送端通过InCh?Mis(0,0)来模拟发送报文丢失，在接收端通过InCh?Mis(0,0)模拟应答报文丢失。如果报文丢失，则需要重发报文。AB协议AB（Alternating Bit）协议是最早的端到端通信协议之一。在AB协议系统中，包含有发送端和接受端两个实体。发送端协议实体从发送方获取一个报文，将序号寄存器值赋给报文，然后向接收端实体发出报文，发送方发出报文之后启动超时时钟，等待认可报文。如果在给定的时间内没有收到认可报文，则重发该报文。如果收到认可报文，其序号与发出报文序号相同，则序号寄存器的内容加1模2，然后发送端实体从发送方用户获取下一个报文；接收端协议实体在收到报文后，如果确认报文无错误，并且序号和序号寄存器的值相等，则向发送端实体发送认可报文（认可报文的序号值等于接收报文的序号值），然后将报文递交给接收方用户，序号寄存器的内容加1模2。如果接收的报文有错误，或者序号不正确，则丢失报文。四实验程序 停止等待协议：#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; /*发送的数据*/byte SendSeq; /*发送序号*/byte ReceivedSeq; /*接收到的报文序号*/SendData=MAXSEQ-1;do :SendData=(SendData+1)%MAXSEQ;again:if :OutCh!Msg(SendData,SendSeq) /*正常发送数据*/ :OutCh!Err(0,0) /*模拟出现无码*/ :OutCh!Miss(0,0) /*模拟丢失*/ fi;if :timeout - goto again :InCh?Miss(0,0) -goto again /*模仿ack丢失，重发报文*/ :InCh?Err(0,0)-goto again /*收到ack误码，重发报文*/ :InCh?Nak(ReceivedSeq,0)- /*收到否定确认，重发报文*/ end1:goto again :InCh?Ack(ReceivedSeq,0)-if /*受到肯定应答，且序号正确发送下一个报文*/ :(ReceivedSeq=SendSeq)-goto progress :(ReceivedSeq!=SendSeq)-end2:goto again /*受到肯定应答，但序号不正确，重发前一个报文*/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)- /*报文按序到达，发送肯定确认*/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=(ExpectedData+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;initrun SENDER(ReceiverToSender,SenderToReceiver);run RECEIVER(SenderToReceiver,ReceiverToSender);AB协议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;