网络协议工程模板.doc

网络协议工程试验汇报
一． 题目描述
1. 将6.3节描述协议条件吗改为: 报文和应答均会犯错, 且都丢失, 接收方没有没有限能力, 这就是我们通常所说使用停等协议。请用PROMELA进行描述, 并用SPIN模拟运行, 通常性验证, 无进展循环验证和认为假如错误进行验证。
2. 请依据图6-16写出著名AB协议PROMELA描述, 并验证“A获取每一个报文最少一次是正确, 而B接收每一个报文至多有一次是正确（Every messages fetched by A is received error-free at least once and accepted at most once by B）”。
二．安装环境
安装spin之前先要安装dev-cpp并配置好系统环境变量。另外, 还需要安装ActiveTcl8.5.11.1.295590-win32-ix86-threaded.exe, 我们所用有窗口界面xspin430.tcl需要用到tcl8.5。下载pc_spin430.zip文件, 解压pc_spin430.zip然后将spin.exe拷贝到比如d:\ spin下, 安装完后还需要配置系统环境变量, 关键是添加gcc目录。
一. 分析
停止等候协议
报文和应答均会犯错, 丢失, 接收方没有没有限接收能力。我们用简单停等协议来处理数据可靠传输问题, 协议关键过程为: 发送方发送报文, 等候应答, 假如是肯定应答则发送下一帧, 假如是否定应答或者应答帧犯错则重发; 接收方接收报文, 假如是期望报文则发送肯定应答, 不然发送否设应答, 给报文加序号。我们将此协议称为RTD4.0。在RTD3.0基础上, 在mtype = {Msg, Ack, Nak, Err, Mis};中添加Mis来模拟报文丢失情况。在发送端经过InCh? Mis(0,0)来模拟发送报文丢失, 在接收端经过InCh? Mis(0,0)模拟应答报文丢失。假如报文丢失, 则需要重发报文。
AB协议
AB（Alternating Bit）协议是最早端到端通信协议之一。在AB协议系统中, 包含有发送端和接收端两个实体。发送端协议实体从发送方获取一个报文, 将序号寄存器值赋给报文, 然后向接收端实体发出报文, 发送方发出报文以后开启超时时钟, 等候认可报文。假如在给定时间内没有收到认可报文, 则重发该报文。假如收到认可报文, 其序号与发出报文序号相同, 则序号寄存器内容加1模2, 然后发送端实体从发送方用户获取下一个报文; 接收端协议实体在收到报文后, 假如确定报文无错误, 而且序号和序号寄存器值相等, 则向发送端实体发送认可报文（认可报文序号值等于接收报文序号值）, 然后将报文递交给接收方用户, 序号寄存器内容加1模2。假如接收报文有错误, 或者序号不正确, 则丢失报文
四．试验程序
停止等候协议:

#define MAXSEQ 5

mtype={Msg,Ack,Nak,Err,Miss};

chan SenderToReceiver=[1]of{mtype,byte,byte};
chan ReceiverToSender=[1]of{mtype,byte,byte};

proctype SENDER(chan InCh,OutCh)
{
byte SendData; /*发送数据*/
byte SendSeq; /*发送序号*/
byte ReceivedSeq; /*接收到报文序号*/
SendData=MAXSEQ-1;
do
::SendData=(SendData+1)%MAXSEQ;
again: if
::OutCh!Msg(SendData,SendSeq) /*正常发送数据*/
::OutCh!Err(0,0) /*模拟出现无码*/
::OutCh!Miss(0,0) /*模拟丢失*/
fi;

if
::timeout -> goto again
::InCh? Miss(0,0) ->goto again /*模仿ack丢失, 重发报文*/
::InCh? Err(0,0)->goto again /*收到ack误码, 重发报文*/
::InCh? Nak(ReceivedSeq,0)-> /*收到否定确定, 重发报文*/
end1: goto again
::InCh? Ack(ReceivedSeq,0)->
if
/*受到肯定应答, 且序号正确发送下一个报文*/
::(ReceivedSeq==SendSeq)->goto progress
::(ReceivedSeq!=SendSeq)->
end2: goto again /*受到肯定应答, 但序号不正确, 重发前一个报文*/
fi
fi;
progress: SendSeq=1-SendSeq; /*产生下一个报文发送序列*/
od;
}

proctype RECEIVER(chan InCh,OutCh)
{
byte ReceivedData; /*接收到报文数据*/
byte ReceivedSeq; /*接收到报文序号*/
byte ExpectedData; /*期望收到报文数据*/
byte ExpectedSeq; /*期望收到报文序号*/
do
::InCh? Msg(ReceivedData,ReceivedSeq)-> /*接收到正常报文*/
if
::(ReceivedSeq==ExpectedSeq)-> /*报文按序抵达, 发送肯定确定*/
assert(ReceivedData==ExpectedData);
progress: ExpectedSeq=1-ExpectedSeq;
ExpectedData=(ExpectedData+1)%MAXSEQ;
if
::OutCh!Miss(0,0); /*模拟ack丢失*/
::OutCh!Ack(ReceivedSeq,0);
::OutCh!Err(0,0); /*模拟ack出现误码*/
ExpectedSeq=1-ExpectedSeq;
ExpectedData=(ExpectedData+4)%MAXSEQ;
fi
::(ReceivedSeq!=ExpectedSeq)->
if
::OutCh!Nak(ReceivedSeq,0); /*报文失序抵达, 发送否定确定*/
::OutCh!Err(0,0); /*模拟nak出现无码*/
fi
fi
::InCh? Err(0,0)->OutCh!Nak(ReceivedSeq,0); /*接收到有误码报文*/
::InCh? Miss(0,0) ->skip;
od;
}

init
{
run SENDER(ReceiverToSender,SenderToReceiver);
run RECEIVER(SenderToReceiver,ReceiverToSender);
}

AB协议
mtype={a,b,err};

chan AtoB=[1]of{mtype,byte};
chan BtoA=[1]of{mtype,byte};

proctype A(chan InCh,OutCh)
{
s5: if
::OutCh!a(0) goto s4;
::OutCh!err(0);
fi;
s4: if
::InCh? err(0)->goto s5;
::InCh? b(0)->goto s1;
::InCh? b(1)->goto s1;
fi;
s1: if
::OutCh!a(1);
::OutCh!err(0);
fi;
goto s2;
s2:
if
::InCh? err(0);goto s5;
::InCh? b(1);goto s1;
::InCh? b(0);goto s3;
fi;
s3: InCh? a(1);
goto s2;
}

proctype B(chan InCh,OutCh)
{
s4: if
::InCh? err(0);goto s5;
::InCh? a(0);goto s1;
::InCh? a(1);goto s1;
fi;
s1: if
::OutCh!b(1);
::OutCh!err(0);
fi;
goto s2;
s2: if
::InCh? err(0);goto s5;
::InCh? a(0);goto s3;
::InCh? a(1);goto s1;
fi;
s3: if
::OutCh!b(1);
::OutCh!err(0);
fi;
goto s2;
s5: if
::OutCh!b(0);
::OutCh!err(0);
fi;
goto s4;
}

init
{
atomic
{
run A(AtoB,BtoA);
run B(BtoA,AtoB);
}
}
五．运行结果

停止等候协议:

模拟运行:

通常性验证:

无进展循环验证:

AB协议:
模拟运行: