网络协议分析上机报告

题目6-5

一， 题目

将 6.3 节描述的协议条件改为：报文和应答均会出错，且都丢失，接收方没有无限接收能力，这就是我们通常所说的实用的停等协议。请用 PROMELA 进行描述，并用 SPIN 模拟运行、一般性验证，无进展循环验证和人为加入错误进验证。

二，分析

相比例 6-3 中的代码， 本题多考虑了一种丢失的情况， 在这里设为 Miss， 且在接受方和发送方的两个进程中添加可能收到 Miss 信息的情况： 当发送方收到 Miss 时， 与收到 Err 的情况相同， 都重发上一个数据； 当接受方接收到 Miss 时， 则直接跳过。

三，代码

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

四，结果

1. 验证

image.png

验证无误

2. 一般性验证：

image.png image.png

3. 无进展循环验证

image.png image.png

4. 运行结果

image.png

题目6-6

一，题目

请根据下图写出著名的 AB 协议的 PROMELA 描述，并验证“A 获取的每一个报文至少有一次是正确的， 而 B 接收的每一个报文至多有一次是正确的 （Every message fetched by A is received error-free at least once and accepted at most once by B）

image.png

二，分析

发送方处于 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接受的每一个报文至多有一次是正确的。

三，代码

mtype = {a,b,Err};
chan AtoB = [1] of {mtype,byte};
chan BtoA = [1] of {mtype,byte};
proctype A(chan InCh,OutCh)
{ S
5:
if
::OutCh!a(0)
::OutCh!Err(0)
fi;
S4:
if
::InCh?b(0) -> goto S1
::InCh?b(1) -> goto S1
::InCh?Err(0) -> goto S5
fi;
S1:
if
::OutCh!a(1)
::OutCh!Err(0)
fi;
S2:
if
::InCh?b(0) -> goto S3
::InCh?b(1) -> goto S1
::InCh?Err(0) -> goto S5
fi;
S3:
if
::OutCh!a(1) -> goto S2
::OutCh!Err(0) -> goto S2
fi;
3
} p
roctype B(chan InCh,OutCh)
{ S
4:
if
::InCh?a(0) -> goto S1
::InCh?a(1) -> goto S1
::InCh?Err(0) -> goto S5
fi;
S1:
if
::OutCh!b(1)
::OutCh!Err(0)
fi;
S2:
if
::InCh?a(0) -> goto S3
::InCh?a(1) -> goto S1
::InCh?Err(0) -> goto S5
fi;
S3:
if
::OutCh!b(1) -> goto S2
::OutCh!Err(0) -> goto S2
fi;
S5:
if
::OutCh!b(0) -> goto S4
::OutCh!Err(0) -> goto S4
fi;
}
init
{
atomic
{
run A(BtoA,AtoB);
run B(AtoB,BtoA);
}
}

四，结果

1. 验证

image.png

验证无误

2. 运行结果

image.png

题目6-7

二， 题目

用PROMELA描述Go-Back-N协议并进行验证

三， 分析

问题分析： GBN 协议的发送方响应三种事件:
(1)上层调用:上层调用 udt_send()时,发送方先检查发送窗口是否已满。 如果未满,则创建 一个分组并发送,否则上层将等待一段时间再试。 (2)ACK 的接收:对序号为 n 的分组的确认用于累计确认(cumulative acknowledgment)。 即 收到序号为 n 的确认分组,则表明 n 之前的报文都正确收到,此时发送方将窗口基序号修改为 n。 (3)超时事件:发送方使用一个定时器,它被最早的已发送但未被确认的分组使用。 如果超 时发生,发送方将重发所有已发送过但还未被确认过的分组。 如果收到一个有效 ACK,则定时 器被重新启动。 GBN协议的接收方动作很简单,如果一个序号为 n的分组被正确收到,并按序,则接收方为 分组 n 发送一个 ACK,并将分组中的数据交付到上层,在所有其他情况下,接收方丢弃该分组并 为最近按序接收的分组重发 ACK。 为研究方便,同时不影响实验目的,在发送方去除了上层调用检查判断发送窗口是否已满 的动作,简化为发送方的 skip 动作,同时,发送方和接收方向上层递交分组不予考虑

四， 代码

#define WIN 4 /*定义窗口大小*/
2 #define MAX 25/*定义发送报文计数最大值*/
3 chan s_r=[10] of {mtype,byte,byte};/*定义发送端到接收端传输通道*/
4 chan r_s=[10] of {mtype,byte,byte};/*定义接收端到发送端传输通道*/
5 mtype={mesg, ack, err};/*定义消息类型*/
6 proctype udt_sender() /*发送端进程*/
7 {
8 byte s,r,swl;/*s 为要发送的报文的序号,r 为确认报文的序号,swl 为滑动窗口下限*/
9 swl = 0; /*窗口初始化*/
10 do::swl = swl;
11 progress:s = swl; /*将要发送报文指针移到窗口头*/
12 progress1: if
13 ::s_r!mesg(0,s)-> /*成功发送正确报文*/
14 (swl<=s)->s = (s+1)%MAX;/*s 后移*/
15 if
16 ::goto progress1; /*在窗口内连续发送*/
17 ::skip/*也可以不发送*/
18 fi;
19 ::s_r!err(s,0) -> /*发送的报文在传输通道中出错*/
20 (swl<=s)->s = (s+1)%MAX;
21 if
22 ::goto progress1;
23 ::skip
24 fi;
25 ::skip -> /*报文在传输通道中丢失*/
26 (swl<=s)->s = (s+1)%MAX;
27 if
28 ::goto progress1;
29 ::skip
30 fi;
31 fi;
32 if
33 ::timeout -> goto progress /*超时,从超时报文开始重发*/
34 ::r_s?err(0,r) -> skip /*收到错误报文不工作*/
35 ::r_s?ack(r,0) ->/*收到正确应答报文*/
36 if
37 ::(r<swl)->skip /*确认序号低于窗口下限*/
38 ::(r>s) -> skip /*高于已发送报文最大值*/
39 ::(swl<=r<=s) -> /*正确确认*/
40 swl = r;/*移动窗口*/
41 goto progress; /*继续发送*/
42 fi;
43 fi;
44 od
45 }
46 proctype udt_receiver()/*接收端进程*/
47 {
48 byte t,es;/*t 为接收报文的序号,es 为期望收到的报文序号*/
49 es = 0; /*初始化*/
50 do
51 ::s_r?mesg(0,t) ->/*收到正确报文*/
52 if
53 ::(t==es)-> /*收到报文为所期望报文*/
54 progress2:es = (es + 1)%MAX;/*更新期望值*/
55 if
56 ::r_s!ack(es,0) /*发送确认*/
57 ::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/
58 ::skip /*确认报文在传输通道中丢失*/
59 fi
60 ::(t!=es)->/*收到无效报文*/
61 if
62 ::r_s!ack(es,0)/*重发确认*/
63 ::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/
64 ::skip /*确认报文在传输通道中丢失*/
65 fi
66 fi
67 ::s_r?err(t,0)->/*收到的报文出错*/
68 if
69 ::r_s!ack(es,0)/*重发确认*/
70 ::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/
71 ::skip /*确认报文在传输通道中丢失*/
72 fi
73 od
74 }
75 init
76 { /*启动进程*/
77 run udt_sender();
78 run udt_receiver();
79 } 验证如下：

五， 结果

1. 验证

image.png

2. 结果

image.png