西电协议分析与设计上机报告模板.docx

协议分析与设计上机汇报

一． 试验目
学习和掌握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=[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)
60 ::OutCh!Err(0)
61 fi;
62 goto S2;
63 S5:
64 if
65 ::OutCh!b(0)
66 ::OutCh!Err(0)
67 fi;
68 goto S4;
69 }
70
71 init
72 {
73 atomic
74 {
75 run A(BtoA,AtoB);
76 run B(AtoB,BtoA);
77 }
78 }

试验截图