一、实验目的
1.熟悉GO-BACK-N协议，并能用PROMELA语言正确描述
2.掌握用SPIN验证协议的方法
二、实验原理
对于给定的一个使用PROMELA描述的协议系统，SPIN可以对其执行任意的模拟，也可以生成一个C代码程序，然后对该系统的正确性进行有效检验，并报告系统中出现的死锁，无效的循环，未定义的接受和标记不完全等情况。
三、实验仪器
PC机
四、实验内容
用PROMELA描述Go-Back-N协议并进行验证
五、实验过程及结果
1.熟悉GO-BACK-N协议
Go-back-N策略的基本原理：当接收方检测出时序的信息后，要求发送方重发最后一个正确接受的信息帧之后的所有未被确认的帧；或者当发送方发送了n个帧后，若发现该n帧的前一帧在计时器超时区间内仍未返回其确认信息，则该帧被判定为出错或丢失，此时发送方不得不重新发送该出错帧及其后的n帧。
在Go-Back-N ARQ中，发送端不需要在接收到上一个数据包的ACK后才发送下一个数据包，而是可以连续发送数据包。在发送端发送数据包的过程中，如果接收到对应已发送的某个数据包的NACK，则发送端将NACK对应的某个数据包进行重发，然后再将该数据包之后的数据包依次进行重发。
GO-Back-N的关键是发送方能够在收到确认之前发送多个分组,但接收方只能缓存一个分组。发送方为发送出去的分组保留副本,直到来自接收方确认达到。
2.用PROMELA语言描述协议
ACK 的接收:收到序号为n的确认分组,则表明n之前的报文都正确收到,此时发送方将窗口基序号修改为n。对序号为 n 的分组的确认用于累计确认。
超时事件:发送方使用一个定时器。如果超时发生,发送方将重发所有已发送过但还未被确认过的分组。如果收到一个有效ACK,则定时器被重新启动。
GBN协议的接收方动作很简单,如果一个序号为 n的分组被正确收到并按序,则接收方为分组n发送一个ACK,并将分组中的数据交付到上层,在所有其他情况下,接收方丢弃该分组并为最近按序接收的分组重发 ACK。

源代码：
1 #define MAXSEQ 5
2 #define SIZE 4
3 mtype={Msg,Ack,Nak,Err,Miss};
4 chan SenderToReceiver=[SIZE] of {mtype,byte,byte};
5 chan ReceiverToSender=[1]of{mtype,byte,byte};
6 proctype SENDER(chan InCh,OutCh)
7 {
8 byte SendData,SDt;
9 byte SendSeq,SSt;
10 byte ReceivedSeq;
11 SendData=0;
12 SendSeq=0;
13 byte count = 0;
14 do
15
16 ::skip->
17 timet: count = count - (SDt-SendData);
18 SSt = SendSeq;
19 SDt=SendData;
20 again: if
21 ::OutCh!Msg(SDt,SSt)
22 ::OutCh!Err(0,0)
23 ::OutCh!Miss(0,0)
24 fi;
25 count = count+1;
26 if
27 :: count<4 ->
28 SDt = SDt+1;
29 SSt = SSt+1;
30 goto again;
31 :: count>=4->
32 count=4;skip;
33 fi;
34 if
35 ::timeout -> goto timet
36 ::InCh?Miss(0,0)->
37 end3: count = count-1; goto again
38 ::InCh?Err(0,0)->
39 end2: count = count -1;goto again
40 ::InCh?Nak(ReceivedSeq,0)->
41 end1: count = count -1;goto again
42 ::InCh?Ack(ReceivedSeq,0)->
43 if
44 ::(ReceivedSeq== SendSeq)->
45 SendSeq = (SendSeq+1)%MAXSEQ;
46 SendData = (SendData+1)%MAXSEQ;
47 count = count-1;
48 ::(ReceivedSeq!=SendSeq)->
49 end4: goto again
50 fi;
51 fi;
52 od;
53 }
54 proctype RECEIVER(chan InCh,OutCh)
55 {
56 byte ReceivedData;
57 byte ReceivedSeq;
58 byte ExpectedData=0;
59 byte ExpectedSeq=0;
60 do
61 ::InCh?Msg(ReceivedData,ReceivedSeq)->
62 if
63 ::(ReceivedSeq==ExpectedSeq)->
64 ExpectedSeq=1+ExpectedSeq;
65 ExpectedData=(ExpectedData+1)%MAXSEQ;
66 if
67 ::OutCh!Miss(0,0)
68 ExpectedSeq=ExpectedSeq-1;
69 ExpectedData=(ExpectedData-1)%MAXSEQ;
70 ::OutCh!Ack(ReceivedSeq,0)
71 ::OutCh!Err(0,0)
72 ExpectedSeq=ExpectedSeq-1;
73 ExpectedData=(ExpectedData-1)%MAXSEQ;
74 fi;
75 ::(ReceivedSeq!=ExpectedSeq)
76 if
77 ::OutCh!Nak(ReceivedSeq,0)
78 ::OutCh!Err(0,0)
79 ::OutCh!Miss(0,0)
80 fi;
81 fi;
82 ::InCh?Err(0,0)
83 if
84 ::OutCh!Nak(ReceivedSeq,0)
85 ::OutCh!Err(0,0)
86 ::OutCh!Miss(0,0)
87 fi;
88 ::InCh?Miss(0,0)->skip;
89 od;
90 }
91 init
92 {
93 atomic
94 {
95 run SENDER(ReceiverToSender,SenderToReceiver);
96 run RECEIVER(SenderToReceiver,ReceiverToSender);
97 }
98 }