资源描述：
《西电协议分析和设计上机报告》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。
1、WORD完美整理版协议分析与设计上机报告范文范例参考指导WORD完美整理版一．实验目的学习和掌握PROMELA语言，并能在SPIN上对协议进行模拟和分析。二．实验题目6-5将6.3节描述的协议条件改为报文和应答均会出错，且都丢失，接收方没有无线接收能力，这就是我们通常所说的实用停等协议。请用PROMELA进行描述，并用SPIN模拟运行、一般性验证、无进展循环验证和人为加入错误进行验证。6-6请根据图6-16写出著名的AB协议的PROMELA描述，并验证“A”获取的每一个报文至少有一个是正确的，而“B”接收的每一个报文之多有一次是正确的。S1?b0?b1S4S3?b1!a1!a0?er
2、r!b1?a0S2?errS5S2?errS5!a1?b0?a1!b1!b0?errS3S1?a0?a1S4TerminalATerminalB三．实验分析6-5停止等待协议因为协议条件为报文应答均会出错，且都丢失，接收方没有无限接收能力，所以此时信道应该有5种信号，分别为：信息，ACK，NAK，出错信号和丢失信号，即mtype={Msg,Ack,Nak,Err,Miss}。范文范例参考指导WORD完美整理版然后定义两个信道，用于在发送方实体和接收方实体进行数据传输。chanSenderToReceiver=[1]of{mtype,byte,byte};chanReceiverToS
3、ender=[1]of{mtype,byte,byte};主要过程为：发送方发送报文，等待应答，如果是肯定应答则发送下一帧，如果是否定应答或者应答帧出错则重发，发送端通过OutCh!Miss(0,0)来模拟发送报文丢失；接收方接收报文，如果是期望的报文则发送肯定应答，否则发送否定应答，接收端通过InCh?Mis(0,0)模拟应答报文丢失，如果报文丢失，则需要重发报文。代码如下：1#defineMAXSEQ523mtype={Msg,Ack,Nak,Err,Miss};4chanSenderToReceiver=[1]of{mtype,byte,byte};5chanReceiverT
4、oSender=[1]of{mtype,byte,byte};67proctypeSENDER(chanInCh,OutCh)8{9byteSendData;10byteSendSeq;11byteReceivedSeq;范文范例参考指导WORD完美整理版12SendData=MAXSEQ-1;13do14::SendData=(SendData+1)%MAXSEQ;15again:if16::OutCh!Msg(SendData,SendSeq)17::OutCh!Err(0,0)18::OutCh!Miss(0,0)19fi;2021if22::timeout->gotoagai
5、n23::InCh?Miss(0,0)->gotoagain24::InCh?Err(0,0)->gotoagain25::InCh?Nak(ReceivedSeq,0)->26end1:gotoagain27::InCh?Ack(ReceivedSeq,0)->28if29::(ReceivedSeq==SendSeq)->gotoprogress30::(ReceivedSeq!=SendSeq)->31end2:gotoagain32fi33fi;范文范例参考指导WORD完美整理版34progress:SendSeq=1-SendSeq;35od;36}3738proctype
6、RECEIVER(chanInCh,OutCh)39{40byteReceivedData;41byteReceivedSeq;42byteExpectedData;43byteExpectedSeq;4445do46::InCh?Msg(ReceivedData,ReceivedSeq)->47if48::(ReceivedSeq==ExpectedSeq)->49assert(ReceivedData==ExpectedData);50progress:ExpectedSeq=1-ExpectedSeq;51ExpectedData=(ExpectedData+1)%MAXSEQ
7、;52if53::OutCh!Miss(0,0)54::OutCh!Ack(ReceivedSeq,0);55::OutCh!Err(0,0);范文范例参考指导WORD完美整理版56ExpectedSeq=1-ExpectedSeq;57ExpectedData=(ExpectedData+4)%MAXSEQ;58fi59::(ReceivedSeq!=ExpectedSeq)->60if61::OutCh!Nak(ReceivedSeq,0);62::O
