协议分析与设计上机报告
一．实验目的
学习和掌握PROMELA语言，并能在SPIN上对协议进行模
拟和分析。
二．实验题目
6-5 将6.3节描述的协议条件改为报文和应答均会出错，且都丢失，接收方没有无线接收能力，这就是我们通常所说的实
用停等协议。请用PROMELA进行描述，并用SPIN模拟运行、
一般性验证、无进展循环验证和人为加入错误进行验证。
6-6 请根据图6-16写出著名的AB协议的PROMELA描述，
并验证“A”获取的每一个报文至少有一个是正确的，而“B”接收的每一个报文之多有一次是正确的。
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
3mtype = {Msg,Ack,Nak,Err,Miss};
4chan SenderToReceiver = [1] of {mtype,byte,byte};
5chan ReceiverToSender = [1] of {mtype,byte,byte};
6
7proctype SENDER(chan InCh,OutCh)
8{
9byte SendData;
10byte SendSeq;
11byte ReceivedSeq;
12SendData = MAXSEQ-1;
13do
14::SendData = (SendData+1)%MAXSEQ;
15again: if
16::OutCh!Msg(SendData,SendSeq)
17::OutCh!Err(0,0)
18::OutCh!Miss(0,0)
19fi;
20
21if
22::timeout -> goto again
23::InCh?Miss(0,0) ->goto again
24::InCh?Err(0,0) ->goto again
25::InCh?Nak(ReceivedSeq,0) ->
26end1: goto again
27::InCh?Ack(ReceivedSeq,0) ->
28if
29::(ReceivedSeq == SendSeq) ->goto progress 30::(ReceivedSeq != SendSeq) ->
31end2:goto again
32fi
33fi;
34progress :SendSeq = 1 - SendSeq;
35od;
36}
37
38proctype RECEIVER(chan InCh,OutCh)
39{
40byte ReceivedData;
41byte ReceivedSeq;
42byte ExpectedData;
43byte ExpectedSeq;
44
45do
46:: InCh?Msg(ReceivedData,ReceivedSeq) ->
47if
48::(ReceivedSeq == ExpectedSeq) ->
49assert(ReceivedData == ExpectedData);
50progress: ExpectedSeq = 1- ExpectedSeq;
51ExpectedData = (ExpectedData + 1)%MAXSEQ; 52if
53::OutCh!Miss(0,0)
54::OutCh!Ack(ReceivedSeq,0);
55::OutCh!Err(0,0);
56ExpectedSeq = 1- ExpectedSeq;
57ExpectedData = (ExpectedData + 4)%MAXSEQ; 58fi
59::(ReceivedSeq!=ExpectedSeq) ->
60if
61::OutCh!Nak(ReceivedSeq,0);
62::OutCh!Err(0,0);
63fi
64fi
65::InCh?Err(0,0) -> OutCh!Nak(ReceivedSeq,0); 66::InCh?Miss(0,0) -> skip
67od;
68}
69
70init
71{
72atomic
73{
74run SENDER(ReceiverToSender,SenderToReceiver); 75run RECEIVER(SenderToReceiver,ReceiverToSender); 76}
77}