文档库

最新最全的文档下载
当前位置:文档库 > 网络协议工程

网络协议工程

网络协议工程实验报告

一.题目描述

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};

网络协议工程

(共9页)