网络协议工程

1、欢迎下载内容仅供参考网络协议工程实验报告一 题目描述将 6.3 节描述的协议条件吗改为：报文和应答均会出错，且都丢失，接收方没有无限能PROMELASPIN一般性验证，无进展循环验证和认为假如错误进行验证。请根据图6-16写出著名的AB协议的PROMELA描述，并验证获取的每一个报文至少一次是正确的，而Bmessages fetched by is received error-free at least once and accepted at most once by 二安装环境spindev-cpp 需要用到tcl8.5。下载pc_spin430.zip 文件，解压pc_spin430.

2、zip 拷贝到例如d: spingcc目录。一. 分析停止等待协议RTD4.0。在RTD3.0 的基础上，在mtype = Msg, Ack, Nak, Err, Mis送端通过InCh?Mis(0,0)来模拟发送报文丢失，在接收端通过InCh?Mis(0,0)模拟应答报文丢失。如果报文丢失，则需要重发报文。AB 协议AB（Alternating Bit）协议是最早的端到端通信协议之一。在AB12，然后发送端实体从发送方用户获取下一个报文；接收端协实体发送认可报文（认可报文的序号值等于接收报文的序号值，然后将报文递交给接收方用1。如果接收的报文有错误，或者序号不正确，则丢失报文。四实验程序停止

3、等待协议： #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)-收到否定确认，重发报end1:goto again:InCh?Ack(ReceivedSeq,0)- if/*受到肯定应答，且序号正确发送下一个报文*/:(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)-认*/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;定确认*/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 协议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!