西电协议分析与设计上机报告

协议分析与设计上机报告一．实验目的学习和掌握PROMELA语言，并能在SPIN上对协议进行模拟和分析。二．实验题目6-5将6.3节描述的协议条件改为报文和应答均会出错，且都丢失，接收方没有无线接收能力，这就是我们通常所说的实用停等协议。请用PROMELA进行描述，并用SPIN模拟运行、一般性验证、无进展循环验证和人为加入错误进行验证。6-6请根据图6-16写出著名的AB协议的PROMELA描述，并验证“A”获取的每一个报文至少有一个是正确的，而“B”接收的每一个报文之多有一次是正确的。S1?b0?b1S4S3?b1!a1!a0?err!b1?a0S2?errS5S2?errS5!a1?b0?a1!b1!b0?errS3S1?a0?a1S4TerminalATerminalB三．实验分析6-5停止等待协议因为协议条件为报文应答均会出错，且都丢失，接收方没有无限接收能力，所以此时信道应该有5种信号，分别为：信息，ACK，NAK，出错信号和丢失信号，即mtype={Msg,Ack,Nak,Err,Miss}。然后定义两个信道，用于在发送方实体和接收方实体进行数据传输。chanSenderToReceiver=[1]of{mtype,byte,byte};chanReceiverToSender=[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};5chanReceiverToSender=[1]of{mtype,byte,byte};67proctypeSENDER(chanInCh,OutCh)8{9byteSendData;10byteSendSeq;11byteReceivedSeq;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-gotoagain23::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;34progress:SendSeq=1-SendSeq;35od;36}3738proctypeRECEIVER(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;52if53::OutCh!Miss(0,0)54::OutCh!Ack(ReceivedSeq,0);55::OutCh!Err(0,0);56ExpectedSeq=1-ExpectedSeq;57ExpectedData=(ExpectedData+4)%MAXSEQ;58fi59::(ReceivedSeq!=ExpectedSeq)-60if61::OutCh!Nak(ReceivedSeq,0);62::OutCh!Err(0,0);63fi64fi65::InCh?Err(0,0)-OutCh!Nak(ReceivedSeq,0);66::InCh?Miss(0,0)-skip67od;68}6970init71{72atomic73{74runSENDER(ReceiverToSender,SenderToReceiver);75runRECEIVER(SenderToReceiver,ReceiverToSender);76}77}实验截图一致性验证:无进展循环验证人为加入错误进行验证6-6AB协议因为根据状态图，S3状态和S1状态一致，所以将S3状态与S1状态合并。在该过程中，一共有3种信号a,b,Err，所以我们定义mtype={a,b,Err}。然后定义两个信道，用于在发送方实体A和接收方实体B进行数据传输。chanAtoB=[1]of{mtype,byte};chanBtoA=[1]of{mtype,byte};主要过程为：发送方处于S5状态，并发送报文a(0)（模拟出错用Err(0)），此时处于S4等待应答。当接收方处于S4并接收到报文，如果是a(0)或者是a(1)则转向S1状态，并发送报文b(1)且转到S2状态；如果是Err(0)则转向S5状态，并发送报文b(0)且转到S4状态。而发送方如果收到的应答是b(0)或者是b(1)则转向S1状态，并发送报文a(1)且转到S2状态。如果是Err(0)则回到S5状态，并发送报文a(0)且转到S4状态。我们假设接受方目前在S2状态并接收到报文，如果是a(0)则转向S3（S1），如果是a(1)则转向S1状态，并发送报文b(1)且转到S2状态；如果是Err(0)则转向S5状态，并发送报文b(0)且转到S4状态。而我们同样假设发送方处于S2状态并接收到报文，如果是b(0)则转向S3（S1），如果是b(1)则转向S1状态，并发送报文a(1)且转到S2状态；如果是Err(0)则转向S5状态，并发送报文a(0)且转到S4状态。所以我们根据分析，能够得到：A获取的每一个报文至少有一次是正确的，而B接受的每一个报文至多有一次是正确的。代码如下：1mtype={a,b,Err};23chanAtoB=[1]of{mtype,byte};4chanBtoA=[1]of{mtype,byte};56proctypeA(chanInCh,OutCh)7{8S5:9if10::OutCh!a(0)11::OutCh!Err(0)12fi;13S4:14if15::InCh?b(0)-gotoS116::InCh?b(1)-gotoS117::InCh?Err-gotoS518fi;19S1:20if21::OutCh!a(1)22::OutCh!Err(0)23fi;24S2:25if26::InCh?b(0)-gotoS327::InCh?b(1)-gotoS128::InCh?Err-gotoS529fi;30S3:31if32::OutCh!a(1)33::OutCh!Err(0)34fi;35gotoS2;36}3738proctypeB(chanInCh,OutCh)39{40S4:41if42::InCh?a(0)-gotoS143::InCh?a(1)-gotoS144::InCh?Err(0)-gotoS545fi;46S1:47if48::OutCh!b(1)49::OutCh!Err(0)50fi;51S2:52if53::InCh?a(0)-gotoS354::InCh?a(1)-gotoS155::InCh?Err(0)-gotoS556fi;57S3:58if59::OutCh!b(1)60::OutCh!Err(0)61fi;62gotoS2;63S5:64if65::OutCh!b(0)66::OutCh!Err(0)67fi;68gotoS4;69}7071init72{73atomic74{75runA(BtoA,AtoB);76runB(AtoB,BtoA);77}78}实验截图