《2022年网络协议工程 .pdf》由会员分享，可在线阅读，更多相关《2022年网络协议工程 .pdf（9页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、网络协议工程实验报告一 题目描述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 on
2、ce 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 的目录。一.分析停止等待协议报文和应答均会出错，丢失，接收方没有无限接收能力。我们用简单的停等协议来解决数据的可靠传输问题，协议主要过程
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。如果接收的报文有错误，或者序号不正确，则丢失报文。四 实验程序停止等待协议：#define M
5、AXSEQ 5 mtype=Msg,Ack,Nak,Err,Miss;chan SenderToReceiver=1ofmtype,byte,byte;chan ReceiverToSender=1ofmtype,byte,byte;名师资料总结-精品资料欢迎下载-名师精心整理-第 1 页，共 9 页 -proctype SENDER(chan InCh,OutCh)byte SendData;/*发送的数据*/byte SendSeq;/*发送序号*/byte ReceivedSeq;/*接收到的报文序号*/SendData=MAXSEQ-1;do:SendData=(SendData+1)
6、%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/*受到
7、肯定应答，且序号正确发送下一个报文*/:(ReceivedSeq=SendSeq)-goto progress:(ReceivedSeq!=SendSeq)-end2:goto again/*受到肯定应答，但序号不正确，重发前一个报文*/fi fi;progress:SendSeq=1-SendSeq;/*产生下一个报文的发送序列*/od;proctype RECEIVER(chan InCh,OutCh)byte ReceivedData;/*接收到的报文数据*/byte ReceivedSeq;/*接收到的报文序号*/byte ExpectedData;/*期望收到的报文数据*/byte
8、ExpectedSeq;/*期望收到的报文序号*/do:InCh?Msg(ReceivedData,ReceivedSeq)-/*接收到正常的报文*/if:(ReceivedSeq=ExpectedSeq)-/*报文按序到达，发送肯定确认*/名师资料总结-精品资料欢迎下载-名师精心整理-第 2 页，共 9 页 -assert(ReceivedData=ExpectedData);progress:ExpectedSeq=1-ExpectedSeq;ExpectedData=(ExpectedData+1)%MAXSEQ;if:OutCh!Miss(0,0);/*模拟 ack 丢失*/:OutC
9、h!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 出现无码*/fi fi:InCh?Err(0,0)-OutCh!Nak(ReceivedSeq,0);/*接收到有误码的报文*/:InCh?Miss(0,0)-skip;
10、od;init run 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 s
11、1;名师资料总结-精品资料欢迎下载-名师精心整理-第 3 页，共 9 页 -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;g
12、oto s2;s2:if:InCh?err(0);goto s5;:InCh?a(0);goto s3;:InCh?a(1);goto s1;fi;s3:if:OutCh!b(1);:OutCh!err(0);fi;goto s2;s5:if:OutCh!b(0);:OutCh!err(0);fi;goto s4;名师资料总结-精品资料欢迎下载-名师精心整理-第 4 页，共 9 页 -init atomic run A(AtoB,BtoA);run B(BtoA,AtoB);五 运行结果停止等待协议：模拟运行：名师资料总结-精品资料欢迎下载-名师精心整理-第 5 页，共 9 页 -一般性验证：名师资料总结-精品资料欢迎下载-名师精心整理-第 6 页，共 9 页 -无进展循环验证：名师资料总结-精品资料欢迎下载-名师精心整理-第 7 页，共 9 页 -AB 协议：模拟运行：名师资料总结-精品资料欢迎下载-名师精心整理-第 8 页，共 9 页 -名师资料总结-精品资料欢迎下载-名师精心整理-第 9 页，共 9 页 -