《网络协议分析与设计》实验报告书实验一

一、实验目的
1.熟悉数据链路层协议，并能用PROMELA语言正确描述
2.掌握用SPIN验证协议的方法
二、实验原理
对于给定的一个使用PROMELA描述的协议系统，SPIN可以对其执行任意的模拟，也可以生成一个C代码程序，然后对该系统的正确性进行有效检验，并报告系统中出现的死锁，无效的循环，未定义的接受和标记不完全等情况。
三、实验仪器
PC机
四、实验内容
将 6.3 节描述的协议条件改为：报文和应答均会出错，且都丢失，接收方没有无限接收能力，这就是我们通常所说的实用的停等协议。请用 PROMELA 进行描述，并用 SPIN 模拟运行、一般性验证，无进展循环验证和人为加入错误进验证。
五、实验步骤及结果
1.熟悉数据链路层协议，分析并相应修改
在课本的第六章的6.3.3已经给出了简单的停等协议，这个协议的条件是报文和应答均会出错，但都不会丢失，接收方没有无限接受能力。该协议的主要过程为：发送方发送数据报，等待应答，如果是肯定应答则发送下一帧，如果是否定应答或应答帧错则重发；接收方接收报文，如果是期望的报文则发送肯定应答。否则发送否定应答，给报文加序号。我们将此协议称为RDT 3.0。
在简单的停等协议的基础上，6-5题多考虑了一种丢失的情况，可以将这种情况设为Miss，且在接受方和发送方的两个进程中添加收到Miss的情况反馈，当发送方收到Miss时，与收到Err的情况相同，都重发上一个数据；当接受方接收到Miss时，则直接跳过。
2.用PROMELA语言描述协议
1 #define MAXSEQ 5
2 mtype={Msg,Ack,Nak,Err,Miss};
3 chan SenderToReceiver=[1]of{mtype,byte,byte};
4 chan ReceiverToSender=[1]of{mtype,byte,byte};
5 proctype SENDER(chan InCh,OutCh)
6 {
7 byte SendData;
8 byte SendSeq;
9 byte ReceivedSeq;
10 SendData=0;
11 SendData=0;
12 do
13 ::skip
14 again: if
15 ::OutCh!Msg(SendData,SendSeq)
16 ::OutCh!Err(0,0)
17 ::OutCh!Miss(0,0)
18 fi;
19 if
20 ::timeout -> goto again
21 ::InCh?Miss(0,0)-> goto again
22 ::InCh?Err(0,0)-> goto again
23 ::InCh?Nak(ReceivedSeq,0)->
24 end1: goto again
25 ::InCh?Ack(ReceivedSeq,0)->
26 if
27 ::(ReceivedSeq== SendSeq)->
28 SendSeq = (SendSeq+1)%MAXSEQ;
29 SendData = (SendData+1)%MAXSEQ;
30 ::(ReceivedSeq!=SendSeq)->
31 end2: goto again
32 fi;
33 fi;
34 od;
35 }
36 proctype RECEIVER(chan InCh,OutCh)
37 {
38 byte ReceivedData;
39 byte ReceivedSeq;
40 byte ExpectedData=0;
41 byte ExpectedSeq;
42 do
43 ::InCh?Msg(ReceivedData,ReceivedSeq)->
44 if
45 ::(ReceivedSeq==ExpectedSeq)->
46 progress: ExpectedSeq=1+ExpectedSeq;
47 ExpectedData=(ExpectedData+1)%MAXSEQ;
48 if
49 ::OutCh!Miss(0,0)
50 ExpectedSeq=ExpectedSeq-1;
51 ExpectedData=(ExpectedData-1)%MAXSEQ;
52 ::OutCh!Ack(ReceivedSeq,0)
53 ::OutCh!Err(0,0)
54 ExpectedSeq=ExpectedSeq-1;
55 ExpectedData=(ExpectedData-1)%MAXSEQ;
56 fi;
57 ::(ReceivedSeq!=ExpectedSeq)
58 if
59 ::OutCh!Nak(ReceivedSeq,0)
60 ::OutCh!Err(0,0)
61 ::OutCh!Miss(0,0)
62 fi;
63 fi;
64 ::InCh?Err(0,0)
65 if
66 ::OutCh!Nak(ReceivedSeq,0)
67 ::OutCh!Err(0,0)
68 ::OutCh!Miss(0,0)
69 fi;
70 ::InCh?Miss(0,0)->skip;
71 od;
72 }
73 init
74 {
75 atomic
76 {
77 run SENDER(ReceiverToSender,SenderToReceiver);
78 run RECEIVER(SenderToReceiver,ReceiverToSender);
79 }
80 }
上述代码的主体部分是和书上的基本一致，只不过是加入MISS的情况。整体分为发送方和接收方两个进程。
在发送方进程，当发送方收到Miss时，与收到Err、收到Nak的情况相同，都goto again，重发上一个数据。
在接收方进程里，大体分为接收到正常的报文、接收有误码的报文、Err和丢失MISS。在接收到正常的报文中，如果出现ACK丢失，则和Err的情况一样，但当接收方接收到Miss时，则直接跳过。
3.用SPIN对协议进行验证
模拟运行：
在Simulate/Replay界面，选择Random，with seed，然后点击“run”，开始协议模拟，点击“stop”暂停模拟。

实用停等协议的模拟运行结果如图：

由于模拟运行的结果中，时序图最为直观明了，所以这里仅仅给出运行过程中产生的时序图来说明模拟运行结果，其他运行结果，例如文本方式，必须经过分析，得到的结论跟时序图是完全一样的。
输出结果如下图所示，从时序图中可以看出协议运行正确。
一般性验证：

在spin中，一般性验证就是选择打开verification界面，然后采取默认选项（穷举状态验证），即safety，然后点击run，开始进行一般性验证。
由图中可以看出，errors：0，说明无一般性验证错误，即该协议通过一般性验证。
从上图也可以看出（橘色框部分），发送方和接收方都在循环执行。
无进展循环验证：
验证结果如下图所示，从图中和源代码分析，可以找出验证不通过的原因是由于发送方发送错误报文后不会改变发送序号，导致发送进程中的process语句不能执行，接收方受到错误报文后也不会改变接收序号，导致接收方的process语句不能执行。但是这是协议要求的情况，是本身协议包含的内容，所以，此处的验证不通过，我们不能把它看做是协议的错误，而是在描述协议正确性要求时，process标签设置不当。

人为加入错误：
为了加深对协议的理解，可人为地在协议描述中添加错误，可以将process去掉，同时添加：：，这就使得发送的报文会出现乱序，验证结果。
在这题中，我将第70行的 ::InCh?Miss(0,0)->skip;改成::InCh?Miss(0,0)->goto again，即对协议进行修改，原来直接可跳过的丢失情况改为重发。经验证，出现错误。

《网络协议分析与设计》实验报告书实验一相关推荐

计算机网络实验：使用Wireshark抓包工具进行网络层和链路层网络协议分析（IP部分）
目录实验名称: 实验介绍: 实验目的: 背景知识和准备: 实验过程: 一. IP协议分析二. Ethernet & ARP 协议分析实验名称: 网络层和链路层网络协议分析实验介绍: 本 ...
计算机网络协议教案,计算机网络实验教案(6)网络协议分析-IP协议3.pdf
计算机网络实验教案(6)网络协议分析-IP协议3.pdf (2页) 本资源提供全文预览,点击全文预览即可全文预览,如果喜欢文档就下载吧,查找使用更方便哦! 9.9 积分 <计算机网络实验> ...
网络协议分析与仿真课程设计报告：网络流量分析与协议模拟
公众号:CS阿吉网络协议分析与仿真课程设计报告题目:网络流量分析与协议模拟专业名称: 网络工程班级: 学生姓名: 阿吉学号(8位): 指导教 ...
《UNIX/Linux网络日志分析与流量监控》实验环境下载
<UNIX/Linux网络日志分析与流量监控>实验环境下载 1.Ossim 4.1 虚拟机下载 (适合2~4G内存的服务器运行),该虚拟机压缩包内包含系统登录密码,Web UI登录密码需 ...
网络协议分析工具Ethereal的使用
大学时计算机网络课的实验报告,当时提不起兴趣,今天看来还挺有用的.可以学习下怎样抓数据包,然后分析程序的通信协议. 一:学习使用网络协议分析工具Ethereal的方法,并用它来分析一些协议. 实验步骤 ...
网络协议分析期末复习专题(二)
期末重点 1.过滤器:区分显示过滤器和捕获过滤器;表达式写监听端口和报文. 2.嗅探:通过集线器,交换机或其他设备进行嗅探;以及嗅探器的位置;网卡可以进行嗅探的原因(混杂模式). 3.网络协议分析:I ...
网络协议分析期末复习专题(一)
期末重点 1.过滤器:区分显示过滤器和捕获过滤器;表达式写监听端口和报文. 2.嗅探:通过集线器,交换机或其他设备进行嗅探;以及嗅探器的位置;网卡可以进行嗅探的原因(混杂模式). 3.网络协议分析:I ...
网络协议分析(最全)
网络协议分析 1.基于Fiddler的HTTP/HTTPS协议分析关于Fiddler: Fiddler是一款由C#开发的免费http调试代理软件,有.net 2和.net 4两种版本.Fi ...
PYTHON黑帽编程1.5 使用WIRESHARK练习网络协议分析
Python黑帽编程1.5 使用Wireshark练习网络协议分析 1.5.0.1 本系列教程说明本系列教程,采用的大纲母本为<Understanding Network Hacks At ...
[转]常用网络协议分析工具
1:TCPDUMP,老牌的分析工具,最先在linux平台使用,现在也可以用于windows平台.命令行方式,2000年以前参加工作者最喜爱的工具,缺点无法分析四层以上协议.常用于检测2-3层网络问题. ...

《网络协议分析与设计》实验报告书实验一

《网络协议分析与设计》实验报告书实验一相关推荐

最新文章

热门文章

《网络协议分析与设计》实验报告书 实验一

《网络协议分析与设计》实验报告书 实验一相关推荐

最新文章

热门文章

《网络协议分析与设计》实验报告书实验一

《网络协议分析与设计》实验报告书实验一相关推荐