西电协议分析实验报告.docVIP

网络协议工程实验报告 姓 名： 纪泽辉 学 号： 030911XX 实验时间： 2012-12-17 实验题目 6-5 将6.3节描述的协议条件改为：报文和应答均会出错，且都丢失，接收方没有无限接收能力，这就是我们通常所说的实用的停等协议。请用PROMELA进行描述，并用SPIN模拟运行、一般性验证，无进展循环验证和人为加入错误进行验证。 6-6 请根据下图写出著名的AB协议的PROMELA描述，并验证“A获取的每一个报文至少有一次是正确的，而B接收的每一个报文至多有一次是正确的（Every message fetched by A is received error-free at least once and accepted at most once by B）” S1 ?b0?b1 S4 S3 ?b1 !a1 !a0 ?err !b1 ?a0 S2 ?err S5 S2 ?err S5 !a1 ?b0 ?a1 !b1 !b0 ?err S3 S1 ?a0 ?a1 S4 Terminal A Terminal B 实验环境搭建 在Windows下安装SPIN，并将spin.exe的路径加入到系统环境变量的Path路径里，然后安装C编译器，经路径加入到系统环境变量Path路径里，然后运行xspin430.tcl，就可编辑程序并进行验证。 实验目的 学习PROMELA语言，并用它描述常见协议并验证。 练习协议验证工具SPIN的使用，并对协议的执行进行模拟。 编程实现 6-5 协议条件为报文应答均会出错且都丢失，因此信道共有五种形式的信号，及发送的数据信号、ACK信号，NAK信号，丢失信号及出错信号。 定义两个信道，用在发送方实体和接收方实体进行数据传送 chan SenderToReceiver=[1]of{mtype,byte,byte}; chan ReceiverToSender=[1]of{mtype,byte,byte} 定义两个进程，分别是发送进程和接收进程，根据协议描述用PROMELA语言编写进程体。当发送方发送的信息后收到NAK，Mis，Err信号之后要重传信号，当收到ACK但ACK信号的序列与发送序列不一致时也要重传，信息丢失，在规定时间内收不到回复时进行超时重传。 接收方在接收到错误信息时返回Err，NAK，或Mis信号，收到正确的期望数据时发送ACK信号。具体程序如下： proctype SENDER(chan InCh,OutCh) { 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; 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)