西电协议详情分析报告与设计上机报告材料.docxVIP

下载本文档

5
0
约4.56千字
约 15页
2018-12-30 发布于安徽
举报
版权申诉

西电协议详情分析报告与设计上机报告材料.docx

1、有哪些信誉好的足球投注网站（book118）网站文档一经付费（服务费），不意味着购买了该文档的版权，仅供个人/单位学习、研究之用，不得用于商业用途，未经授权，严禁复制、发行、汇编、翻译或者网络传播等，侵权必究。。
2、本站所有内容均由合作方或网友上传，本站不对文档的完整性、权威性及其观点立场正确性做任何保证或承诺！文档内容仅供研究参考，付费前请自行鉴别。如您付费，意味着您自己接受本站规则且自行承担风险，本站不退款、不进行额外附加服务；查看《如何避免下载的几个坑》。如果您已付费下载过本站文档，您可以点击这里二次下载。
3、如文档侵犯商业秘密、侵犯著作权、侵犯人身权等，请点击“版权申诉”（推荐），也可以打举报电话：400-050-0827(电话支持时间：9:00-18:30)。
4、该文档为VIP文档，如果想要下载，成为VIP会员后，下载免费。
5、成为VIP后，下载本文档将扣除1次下载权益。下载后，不支持退款、换文档。如有疑问请联系我们。
6、成为VIP后，您将拥有八大权益，权益包括：VIP文档下载权益、阅读免打扰、文档格式转换、高级专利检索、专属身份标志、高级客服、多端互通、版权登记。
7、VIP文档为合作方或网友上传，每下载1次，网站将根据用户上传文档的质量评分、类型等，对文档贡献者给予高额补贴、流量扶持。如果你也想贡献VIP文档。上传文档

协议分析与设计上机报告实验目的学习和掌握PROMELA语言，并能在SPIN上对协议进行模拟和分析。实验题目 6-5 将6.3节描述的协议条件改为报文和应答均会出错，且都丢失，接收方没有无线接收能力，这就是我们通常所说的实用停等协议。请用PROMELA进行描述，并用SPIN模拟运行、一般性验证、无进展循环验证和人为加入错误进行验证。 6-6 请根据图6-16写出著名的AB协议的PROMELA描述，并验证“A”获取的每一个报文至少有一个是正确的，而“B”接收的每一个报文之多有一次是正确的。 S1 ?b0?b1 S4 S3 ?b1 !a1 !a0 ?err !b1 ?a0 S2 ?err S5 S2 ?err S5 !a1 ?b0 ?a1 !b1 !b0 ?err S3 S1 ?a0 ?a1 S4 Terminal A Terminal B 实验分析 6-5 停止等待协议因为协议条件为报文应答均会出错，且都丢失，接收方没有无限接收能力，所以此时信道应该有5种信号，分别为：信息，ACK，NAK，出错信号和丢失信号，即mtype={Msg,Ack,Nak,Err,Miss}。然后定义两个信道，用于在发送方实体和接收方实体进行数据传输。 chan SenderToReceiver=[1]of{mtype,byte,byte}; chan ReceiverToSender=[1]of{mtype,byte,byte}; 主要过程为：发送方发送报文，等待应答，如果是肯定应答则发送下一帧，如果是否定应答或者应答帧出错则重发，发送端通过OutCh!Miss(0,0) 来模拟发送报文丢失；接收方接收报文，如果是期望的报文则发送肯定应答，否则发送否定应答，接收端通过InCh?Mis(0,0)模拟应答报文丢失，如果报文丢失，则需要重发报文。代码如下： 1 #define MAXSEQ 5 2 3 mtype = {Msg,Ack,Nak,Err,Miss}; 4 chan SenderToReceiver = [1] of {mtype,byte,byte} ; 5 chan ReceiverToSender = [1] of {mtype,byte,byte} ; 6 7 proctype SENDER(chan InCh,OutCh) 8 { 9 byte SendData; 10 byte SendSeq; 11 byte ReceivedSeq; 12 SendData = MAXSEQ-1; 13 do 14 ::SendData = (SendData+1)%MAXSEQ; 15 again: if 16 ::OutCh!Msg(SendData,SendSeq) 17 ::OutCh!Err(0,0) 18 ::OutCh!Miss(0,0) 19 fi; 20 21 if 22 ::timeout - goto again 23 ::InCh?Miss(0,0) -goto again 24 ::InCh?Err(0,0) -goto again 25 ::InCh?Nak(ReceivedSeq,0) - 26 end1: goto again 27 ::InCh?Ack(ReceivedSeq,0) - 28 if 29 ::(ReceivedSeq == SendSeq) -goto progress 30 ::(ReceivedSeq != SendSeq) - 31 end2: goto again 32 fi 33 fi; 34 progress : SendSeq = 1 - SendSeq; 35 od; 36 } 37 38 proctype RECEIVER(chan InCh,OutCh) 39 { 40 byte ReceivedData; 41 byte ReceivedSeq; 42 byte ExpectedData; 43 byte ExpectedSeq; 44 45 do 46 :: InCh?Msg(ReceivedData,ReceivedSeq) - 47