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

实用标准协议分析与设计上机报告一 实验目的学习和掌握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=1ofmtype,byte,byte;chan ReceiverToSender=1ofmtype,byte,byte;主要过程为：发送方发送报文，等待应答，如果是肯定应答则发送下一帧，如果是否定应答或者应答帧出错则重发，发送端通过OutCh!Miss(0,0) 来模拟发送报文丢失；接收方接收报文，如果是期望的报文则发送肯定应答，否则发送否定应答，接收端通过InCh?Mis(0,0)模拟应答报文丢失，如果报文丢失，则需要重发报文。代码如下：1#define MAXSEQ 523mtype = Msg,Ack,Nak,Err,Miss;4chan SenderToReceiver = 1 of mtype,byte,byte;5chan ReceiverToSender = 1 of mtype,byte,byte;67proctype SENDER(chan InCh,OutCh)89byte SendData;10byte SendSeq;11byte ReceivedSeq;12SendData = MAXSEQ-1;13do14 :SendData = (SendData+1)%MAXSEQ;15again: if16:OutCh!Msg(SendData,SendSeq)17:OutCh!Err(0,0)18:OutCh!Miss(0,0)19 fi;2021 if22:timeout - goto again23:InCh?Miss(0,0) -goto again24:InCh?Err(0,0) -goto again25:InCh?Nak(ReceivedSeq,0) -26end1: goto again27:InCh?Ack(ReceivedSeq,0) -28if29:(ReceivedSeq = SendSeq) -goto progress30:(ReceivedSeq != SendSeq) -31 end2:goto again32fi33fi;34progress :SendSeq = 1 - SendSeq;35od;363738proctype RECEIVER(chan InCh,OutCh)3940byte ReceivedData;41byte ReceivedSeq;42byte ExpectedData;43byte ExpectedSeq;4445do46: InCh?Msg(ReceivedData,ReceivedSeq) -47if 48:(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) -60 if61 :OutCh!Nak(ReceivedSeq,0);62 :OutCh!Err(0,0);63 fi64fi65:InCh?Err(0,0) - OutCh!Nak(ReceivedSeq,0);66:InCh?Miss(0,0) - skip67od;686970init 7172atomic7374run SENDER(ReceiverToSender,SenderToReceiver);75run RECEIVER(SenderToReceiver,ReceiverToSender);7677实验截图一致性验证:无进展循环验证人为加入错误进行验证6-6 AB协议因为根据状态图，S3状态和S1状态一致，所以将S3状态与S1状态合并。在该过程中，一共有3种信号a,b,Err，所以我们定义mtype = a,b,Err。然后定义两个信道，用于在发送方实体A和接收方实体B进行数据传输。chan AtoB = 1 of mtype,byte;chan BtoA = 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;23chan AtoB = 1 of mtype,byte;4chan BtoA = 1 of mtype,byte;56proctype A(chan InCh,OutCh)78S5:9if10:OutCh!a(0) 11:OutCh!Err(0)12fi;13S4:14if15:InCh?b(0) - goto S116:InCh?b(1) - goto S117:InCh?Err - goto S518fi;19S1:20if21:OutCh!a(1)22:OutCh!Err(0)23fi;24S2:25if26:InCh?b(0) - goto S327:InCh?b(1) - goto S128:InCh?Err - goto S529fi;30S3:31if32:OutCh!a(1)33:OutCh!Err(0)34fi;35goto S2;363738proctype B(chan InCh,OutCh)3940S4:41 if 42:InCh?a(0) - goto S143:InCh?a(1) - goto S144:InCh?Err(0) - goto S545fi;46S1:47if48:OutCh!b(1)49:OutCh!Err(0)50fi;51S2:52if53:InCh?a(0) - goto S354:InCh?a(1) - goto S155:InCh?Err(0) - got