协议分析与设计上机报告 一． 实验目的 学习和掌握PROMELA语言，并能在SPIN上对协议进行模拟和分析。 二． 实验题目 6-5 将6.3节描述的协议条件改为报文和应答均会出错，且都丢失，接收方没有无线接收能力，这就是我们通常所说的实用停等协议。请用PROMELA进行描述，并用SPIN模拟运行、一般性验证、无进展循环验证和人为加入错误进行验证。 6-6 请根据图6-16写出著名的AB协议的PROMELA描述，并验证“A”获取的每一个报文至少有一个是正确的，而“B”接收的每一个报文之多有一次是正确的。

S1 b0b1 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 if 48 ::(ReceivedSeq == ExpectedSeq) -> 49 assert(ReceivedData == ExpectedData); 50 progress: ExpectedSeq = 1- ExpectedSeq; 51 ExpectedData = (ExpectedData + 1)%MAXSEQ; 52 if 53 ::OutCh!Miss(0,0) 54 ::OutCh!Ack(ReceivedSeq,0); 55 ::OutCh!Err(0,0); 56 ExpectedSeq = 1- ExpectedSeq; 57 ExpectedData = (ExpectedData + 4)%MAXSEQ; 58 fi 59 ::(ReceivedSeq!=ExpectedSeq) -> 60 if 61 ::OutCh!Nak(ReceivedSeq,0); 62 ::OutCh!Err(0,0); 63 fi 64 fi 65 ::InCh?Err(0,0) -> OutCh!Nak(ReceivedSeq,0); 66 ::InCh?Miss(0,0) -> skip 67 od; 68 } 69 70 init 71 { 72 atomic 73 { 74 run SENDER(ReceiverToSender,SenderToReceiver); 75 run RECEIVER(SenderToReceiver,ReceiverToSender); 76 } 77 } 实验截图 一致性验证: 无进展循环验证 人为加入错误进行验证 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接受的每一个报文至多有一次是正确的。 代码如下： 1 mtype = {a,b,Err}; 2 3 chan AtoB = [1] of {mtype,byte}; 4 chan BtoA = [1] of {mtype,byte}; 5 6 proctype A(chan InCh,OutCh) 7 { 8 S5: 9 if 10 ::OutCh!a(0) 11 ::OutCh!Err(0) 12 fi; 13 S4: 14 if 15 ::InCh?b(0) -> goto S1 16 ::InCh?b(1) -> goto S1 17 ::InCh?Err -> goto S5 18 fi; 19 S1: 20 if 21 ::OutCh!a(1) 22 ::OutCh!Err(0) 23 fi; 24 S2: 25 if 26 ::InCh?b(0) -> goto S3 27 ::InCh?b(1) -> goto S1 28 ::InCh?Err -> goto S5 29 fi; 30 S3: 31 if 32 ::OutCh!a(1) 33 ::OutCh!Err(0) 34 fi; 35 goto S2; 36 } 37 38 proctype B(chan InCh,OutCh) 39 { 40 S4: 41 if 42 ::InCh?a(0) -> goto S1 43 ::InCh?a(1) -> goto S1 44 ::InCh?Err(0) -> goto S5 45 fi; 46 S1: 47 if 48 ::OutCh!b(1) 49 ::OutCh!Err(0) 50 fi; 51 S2: 52 if 53 ::InCh?a(0) -> goto S3 54 ::InCh?a(1) -> goto S1 55 ::InCh?Err(0) -> goto S5 56 fi; 57 S3: 58 if 59 ::OutCh!b(1)