西电协议分析上机报告.doc

发布时间：2022-06-13 发布人：admin 分类：说明书资料大小：0.22M 资料格式：doc 举报版权申诉

65c1e744-2113-40d3-a5eb-c96fb785f560.doc.pdf-第1页.png

第1页 / 共13页

65c1e744-2113-40d3-a5eb-c96fb785f560.doc.pdf-第2页.png

第2页 / 共13页

65c1e744-2113-40d3-a5eb-c96fb785f560.doc.pdf-第3页.png

第3页 / 共13页

65c1e744-2113-40d3-a5eb-c96fb785f560.doc.pdf-第4页.png

第4页 / 共13页

65c1e744-2113-40d3-a5eb-c96fb785f560.doc.pdf-第5页.png

第5页 / 共13页

65c1e744-2113-40d3-a5eb-c96fb785f560.doc.pdf-第6页.png

第6页 / 共13页

65c1e744-2113-40d3-a5eb-c96fb785f560.doc.pdf-第7页.png

第7页 / 共13页

65c1e744-2113-40d3-a5eb-c96fb785f560.doc.pdf-第8页.png

第8页 / 共13页

文本预览

协议分析与设计上机报告学号:13030288014 姓名：宋慧鹏

一、本实验课程的教学目标与任务计算机网络及通信系统的核心技术是协议分析与设计。协议分析与设计是借助计算机，在相应软件平台上对以 PROMELA 语言为描述手段完成的设计规范，自动地完成相应协议仿真，模拟，验证测试，从而减少协议开发过程中存在的错误，提高协议开发的效率和质量。因此，学习协议分析与设计对计算机网络及通信系统十分重要。本课程的主要任务是：通过上机实验使学生掌握计算机网络及通信系统的协议分析方法，培养学生协议分析及工程实践能力。二、本课程与其他课程的联系和分工相关课程如计算机网络，数据通信，分布式系统等。计算机网络等其他的课程一般只涉及介绍经国际标准化组织标准化的协议，而协议与分析着重于让读者熟悉协议开发过程中的基本概念，方法和技术。三、实验课程内容和基本要求（一）试验设备与工具软件（上机环境与工具软件）（1）实验所需仪器设备：计算机。（2）实验所需工具软件：SPIN。（二）具体内容基于 PROMELA 语言的协议分析验证用 PROMELA 语言描述以下协议并进行模拟仿真与协议验证，检测协议的正确性： (1)数据链路层协议 (2)AB 协议 (3)GO-BACK-N 协议

（三）基本要求 (1)熟悉工具软件 SPIN 的安装与使用 (2)掌握用 PROMELA 语言对协议进行描述的方法实验一一、实验目的（明确学生应达到的基本能力要求） 1.熟悉数据链路层协议，并能用 PROMELA 语言正确描述 2.掌握用 SPIN 验证协议的方法二、实验原理对于给定的一个使用 PROMELA 描述的协议系统，SPIN 可以对其执行任意的模拟，也可以生成一个 C 代码程序，然后对该系统的正确性进行有效检验，并报告系统中出现的死锁，无效的循环，未定义的接受和标记不完全等情况。三、实验仪器 PC 机四、实验内容及步骤实验内容：熟悉数据链路层协议，并将协议条件修改为：报文和应答均会出错，且都丢失，接受方没有无限接受能力。实验步骤： 1.熟悉数据链路层协议，并进行相应修改 2.用 PROMELA 语言描述协议 3.用 SPIN 对协议进行验证五、实验结果代码： #define MAXSEQ mtype={Msg,Ack,Nak,Err,Miss}; chan SenderToReceiver=[1]of{mtype,byte,byte}; chan ReceiverToSender=[1]of{mtype,byte,byte}; 5

proctype Sender(chan InCh;chan OutCh) { byte SenderData; byte SenderSeq; byte ReceiverSeq; SenderData = MAXSEQ-1; do ::SenderData=(SenderData+1)%MAXSEQ; again: if ::OutCh ! Msg(SenderData,SenderSeq); ::OutCh ! Err(0,0); ::OutCh ! Miss(0,0); fi; if ::InCh ? Ack(ReceiverSeq,0)-> goto progress ; if fi ::(ReceiverSeq == SenderSeq) -> ::(ReceiverSeq != SenderSeq) -> end1: goto again ; ::InCh ? Nak(ReceiverSeq,0)-> end2: goto again; ::InCh ? Err(0,0) -> end3: goto again; ::InCh ? Miss(0,0) -> end4: goto again; ::timeout -> end5: goto again; fi;

progress: SenderSeq = 1-SenderSeq ; od } proctype Receiver(chan InCh;chan OutCh) { byte ReceiverData; byte ReceiverSeq; byte ExceptedData; byte ExceptedSeq; do ::InCh ? Msg(ReceiverData,ReceiverSeq) -> if ::(ReceiverSeq == ExceptedSeq)-> assert(ReceiverData == ExceptedData); progress: ExceptedSeq = 1-ExceptedSeq; ExceptedData= (ExceptedData+1)%MAXSEQ; if ::OutCh ! Ack(ReceiverSeq,0); ::OutCh ! Err(0,0); ExceptedSeq = 1-ExceptedSeq; ExceptedData=(ExceptedData+4)%MAXSEQ ::OutCh ! Miss(0,0); ExceptedSeq = 1-ExceptedSeq; ExceptedData=(ExceptedData+4)%MAXSEQ

fi ::(ReceiverSeq != ReceiverSeq)-> if fi ::OutCh ! Nak(ReceiverSeq,0); ::OutCh ! Err(0,0); ::OutCh ! Miss(0,0); fi ::InCh ? Err(0,0) -> OutCh ! Nak(ReceiverSeq,0) ::InCh ? Miss(0,0)-> skip od } init { atomic{ run Sender(ReceiverToSender,SenderToReceiver); run Receiver(SenderToReceiver,ReceiverToSender); } } 结果：

实验二一、实验目的（明确学生应达到的基本能力要求） 1.熟悉 AB 协议，并能用 PROMELA 语言正确描述 2.掌握用 SPIN 验证协议的方法二、实验原理对于给定的一个使用 PROMELA 描述的协议系统，SPIN 可以对其执行任意的模拟，也可以生成一个 C 代码程序，然后对该系统的正确性进行有效检验，并报告系统中出现的死锁，无效的循环，未定义的接受和标记不完全等情况。三、实验仪器 PC 机四、实验内容及步骤实验内容：熟悉 AB 协议，并根据状态图用 PROMELA 语言描述该协议实验步骤： 1.熟悉 AB 协议 2.用 PROMELA 语言描述协议 3.用 SPIN 对协议进行验证五、实验结果代码： mtype = {err,a,b} chan SenderToReceiver = [1]of{mtype,byte}; chan ReceiverToSender = [1]of{mtype,byte}; proctype A(chan InCh;chan OuCh) { S5: if fi; ::OuCh ! a(0) -> goto S4 ::OuCh ! err(0)

-> goto S1 ::InCh ? b(0) ::InCh ? b(1) -> goto S1 ::InCh ? err(0) -> goto S5 S4: if fi; S1: if ::OuCh ! a(1) ::OuCh ! err(0) fi; goto S2; S2: if -> goto S3 ::InCh ? b(0) ::InCh ? b(1) -> goto S1 ::InCh ? err(0) -> goto S5 fi; S3: if fi ::OuCh ! a(1) -> goto S2 } proctype B(chan InCh;chan OuCh) { if ::InCh?err(0) -> goto S5 ::InCh?a(0) -> goto S1 -> goto S1 ::InCh?a(1)

分享到：

赞收藏

资料库

西电协议分析上机报告.doc

相关推荐

课程资源

热门标签

最新资料