2022年网络协议分析 .pdf

资源ID：33396061 资源大小：70.96KB 全文页数：15页
资源格式： PDF 下载积分：4.3金币

快捷下载

会员登录下载

微信登录下载

三方登录下载：

微信扫一扫登录

下载资源需要4.3金币

邮箱/手机：
温馨提示：	快捷下载时，用户名和密码都是您填写的邮箱或者手机号，方便查询和重复下载（系统自动生成）。如填写123，账号就是123，密码也是123。
支付方式：
验证码：	换一换

账号：
密码：
验证码：	换一换
当日自动登录忘记密码？

友情提示

1、下载资料失败解决办法

2、PDF文件下载后，可能会被浏览器默认打开，此种情况可以点击浏览器菜单，保存网页到桌面，就可以正常下载了。

3、本站不支持迅雷下载，请使用电脑自带的IE浏览器，或者360浏览器、谷歌浏览器下载即可。

4、本站资源下载后的文档和图纸-无水印,预览文档经过压缩，下载后原文更清晰。

5、试题试卷类文档，如果标题没有明确说明有答案则都视为没有答案，请知晓。

网站客服

侵权投诉

2022年网络协议分析 .pdf

网络协议分析姓名学号：班级名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 1 页，共 15 页 - - - - - - - - - 一、实验题目(1) 验证数据链路层协议的安全性(2)AB 协议(3)GO-BACK-N协议二、实验环境搭载在 windows 下安装 spin ，将 spin.exe的路径添加到环境变量path中，若电脑有 gcc，则直接将其路径写入path，若无则安装 Dev-c+，将其内所包含的gcc 写入 path 。然后运行 xspin525.tcl，即可启动spin 完成实验。三、实验目的 1. 学习 PROMELA语言，并用它描述常见协议并验证。 2. 练习协议工具 spin 的使用，并对协议的执行进行模拟。四、编程实现 1.数据链路层的协议正确性验证协议条件分为报文应答会出错且丢失，因此信道共有五中形式的信号，即发送的数据信号、ACK信号、 NAK信号，丢失信号和出错信号；定义两个信道，用在发送方实体和接收方实体进行数据传送；定义两个进程，分别是发送方进程和接受进程，发送方在接受到错误的信号或 ACK序列号不匹配时，进行重传。接收方，收到错误信息时，发送 Err ，NAK ，Mis 信号，正确时返回ACK信号。具体程序如下：proctype SENDER(chan InCh,OutCh) 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 2 页，共 15 页 - - - - - - - - - byte SendData; byte SendSeq; byte ReceivedSeq; SendData=5-1; do :SendData=(SendData+1)%5; again: if :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!Err(0,0) :OutCh!Mis(0,0) fi; 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 3 页，共 15 页 - - - - - - - - - if :timeout - goto again :InCh?Mis(0,0) - goto again :InCh?Err(0,0)-goto again :InCh?Nak(ReceivedSeq,0)- 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)- 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 4 页，共 15 页 - - - - - - - - - assert(ReceivedData=ExpectedData); progress: ExpectedSeq=1-ExpectedSeq; ExpectedData=(ExpectedData+1)%5; if :OutCh!Mis(0,0) :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Ack(ReceivedSeq,0); :OutCh!Err(0,0); ExpectedSeq=1-ExpectedSeq; ExpectedData=(ExpectedData+4)%5; fi :(ReceivedSeq!=ExpectedSeq)- 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 5 页，共 15 页 - - - - - - - - - if :OutCh!Mis(0,0); :OutCh!Nak(ReceivedSeq,0); :OutCh!Err(0,0); fi fi :InCh?Err(0,0)-OutCh!Nak(ReceivedSeq,0); :InCh?Mis(0,0) - skip; od; init run SENDER(ReceiverToSender,SenderToReceiver); run RECEIVER(SenderToReceiver,ReceiverToSender); 2.AB 协议根据 AB协议状态转换图用PROMELA 语言进行描述。其中由于S1状态和 S3状态发送的信息是一致的，故将两个状态合一。定义两个发送和两个接收进程，分为A发送 B接收，B发送 A接收。具体程序如下：名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 6 页，共 15 页 - - - - - - - - - mtype = Err,a,b; chan SenderToReceiver = 1 of mtype,byte; chan ReceiverToSender = 1 of mtype,byte; proctype A_SENDER(chan InCh, OutCh) S5: if :OutCh!a(0) :OutCh!Err(0) fi; 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; if :InCh?Err(0)- goto S5 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 7 页，共 15 页 - - - - - - - - - :InCh? b(1)- goto S1 :InCh?b(0)- goto S1 fi; proctype B_RECEIVER(chan InCh, OutCh) if :InCh?Err(0)- goto S5 :InCh?a(0) - goto S1 :InCh?a(1)- goto S1 fi; S5: if :OutCh!b(0) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 :InCh?a(0) - goto S1 :InCh?a(1)- goto S1 fi; S1: if 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 8 页，共 15 页 - - - - - - - - - :OutCh!b(1) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 :InCh?a(1)- goto S1 :InCh?a(0)- goto S1 fi; proctype B_SENDER(chan InCh, OutCh) S5: if :OutCh!b(0) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 :InCh?a(0) - goto S1 :InCh?a(1)- goto S1 fi; S1: if 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 9 页，共 15 页 - - - - - - - - - :OutCh!b(1) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 :InCh?a(1)- goto S1 :InCh?a(0)- goto S1 fi; proctype A_RECEIVER(chan InCh, OutCh) if :InCh?Err(0)- goto S5 :InCh?b(0)- goto S1 :InCh?b(1)- goto S1 fi; S5: if :OutCh!a(0) :OutCh!Err(0) fi; if 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 10 页，共 15 页 - - - - - - - - - :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; if :InCh?Err(0)- goto S5 :InCh? b(1)- goto S1 :InCh?b(0)- goto S1 fi; init atomic run A_SENDER(ReceiverToSender,SenderToReceiver); run B_RECEIVER(SenderToReceiver, ReceiverToSender); 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 11 页，共 15 页 - - - - - - - - - /* atomic run B_SENDER(ReceiverToSender,SenderToReceiver); run A_RECEIVER(SenderToReceiver, ReceiverToSender); */ 3.GO-BACK-N协议（1）初始化。开网络层允许； ack_expected = 0（此时处于发送窗口的下沿）； next_frame_to_send = 0，frame_expected = 0（初始化正在发送的帧和期待的帧序号）； nbuffered = 0（进行发送窗口大小初始化）；（2）等待事件发生（网络层准备好，帧到达，收到坏帧，超时）。（3）如果事件为网络层准备好，则执行以下步骤。从网络层接收一个分组，放入相应的缓冲区；发送窗口大小加1 ；使用缓冲区中的数据分组、 next_frame_to_send和frame_expected 构造帧，继续发送； next_frame_to_send加 1；跳转（7）；（4）如果事件为帧到达，则从物理层接收一个帧，则执行以下步骤。名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 12 页，共 15 页 - - - - - - - - - 首先检查帧的 seq 域，若正是期待接收的帧（seq = frame_expected ），将帧中携带的分组交给网络层，frame_expected 加 1；然后检查帧的 ack 域，若 ack 落于发送窗口内，表明该序号及其之前所有序号的帧均已正确收到，因此终止这些帧的计时器，修改发送窗口大小及发送窗口下沿值将这些帧去掉，继续执行步骤（7）；（5）如果事件是收到坏帧，继续执行步骤（7）。（6）如果事件是超时，即： next_frame_to_send = ack_expected，从发生超时的帧开始重发发送窗口内的所有帧，后继续执行步骤（7）。（7）若发送窗口大小小于所允许的最大值（MAX-SEQ），则可继续向网络层发送，否则则暂停继续向网络层发送，同时返回互步骤（2）等待。具体程序如下：#define MaxSeq 3 #define Wrong(x) x = (x+1) % (MaxSeq) #define Right(x) x = (x+1) % (MaxSeq + 1) #define inc(x) Right(x) 5 chan q2 = MaxSeq of byte, byte ; active 2 proctype p5() 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 13 页，共 15 页 - - - - - - - - - byte NextFrame, AckExp, FrameExp, r, s, nbuf, i; chan in, out; in = q_pid; out = q1-_pid; xr in; xs out; do : nbuf nbuf+; out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); inc(NextFrame) : q_pid?r,s - if : r = FrameExp - printf(MSC: accept %dn, r) inc(FrameExp) : else fi; do : (AckExp = s) & (s NextFrame)|(AckExp = s) & (NextFrame AckExp)|(s NextFrame) & (NextFrame nbuf-; 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 14 页，共 15 页 - - - - - - - - - inc(AckExp); : else - break od : timeout - NextFrame = AckExp; printf(MSC: timeoutn); i = 1; do : i out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); inc(NextFrame); i+ : else - break od 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 15 页，共 15 页 - - - - - - - - -

注意事项

本文（2022年网络协议分析 .pdf）为本站会员（H****o）主动上传，淘文阁 - 分享文档赚钱的网站仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若此文所含内容侵犯了您的版权或隐私，请立即通知淘文阁 - 分享文档赚钱的网站（点击联系客服），我们立即给予删除！

温馨提示：如果因为网速或其他原因下载失败请重新下载，重复下载不扣分。