第6章-协议验证工具

第6章协议验证工具第5章协议验证技术2内容提要SPIN概述1PROMELA语言2SPIN应用3第5章协议验证技术3SPINSPIN（SimplePromelaInterpreter）是一种适用于分布式软件系统的形式化验证的开源软件工具：用C语言开发的模型检查工具SPIN的开发者GerardJ.Holzmann获得了ACM2001年度软件系统奖(SoftwareSystemsAward)第5章协议验证技术4SPINSPIN特点SPIN对用Promela语言描述的网络协议设计规格说明（Specification）的逻辑一致性进行检验，并报告系统中出现的死锁、无效的循环、未定义的接收和标记不完全等情况SPIN无需构建一个全局的状态图，而可以根据需要生成系统自动机的部分状态进行检验（on-the-fly技术）SPIN支持同步和异步两种通信方式对于给定的一个使用PROLEMA描述的协议系统，SPIN可以对其执行任意的模拟，也可以生成一个C代码程序，然后对该系统的正确性进行有效的检验适于不同规模的系统的验证第5章协议验证技术5内容提要SPIN概述1PROMELA语言2SPIN应用3第5章协议验证技术6PROMELA语言在SPIN中，将描述协议实体间所有交互过程的协议描述称为验证模型（validationmodel），而将描述验证模型的语言称为PROMELA(Protocol/ProcessMetaLanguage)PROMELA是一种类似于C程序设计语言的形式描述语言，它可以方便地描述形式化验证模型中的系统的各种行为。一个用PROMELA描述的协议验证模型由三类对象构成：进程（processes）、报文通道（messagechannels）、状态变量（statevariables）所有进程被定义为全局对象，而报文通道和状态变量则是进程使用的全局或局部数据。实际上，验证模型相当于一个前面所述的有限状态机详细内容见本书第六章第5章协议验证技术7内容提要SPIN概述1PROMELA语言2SPIN应用3第5章协议验证技术8SPIN安装Spin验证器有两种版本：windows版和Linux版，且两个版本均有相应的图形框架支持，前者使用jspin或xspin，后者使用ispin实现。jSpin采用基于java开发的可视化框架，可直接运行于windows平台，但其没有图形化的仿真工具，无法直观看到协议运行的过程。XSpin运行于Cygwin平台上，利用类UNIX的命令行方式启动。Xspin启动成功后仍然可以使用图形化的操作方式。第5章协议验证技术9Windows下安装1.下载相关软件：spin,Xspin,和tcl,，其中tcl区分64位和32位，下载时注意区别，下载的软件是：xspin430.tcl，pc_spin430,ActiveTcl8.5.11.1.295590-win32-ix86-threaded.exetcl下载地址：，spin下载地址：。2.安装ActiveTcl8.5.11.1.295590-win32-ix86-threaded.exe3.配置环境变量首先将下载的spin加入PATH路径再将gcc编译器写入PATH，如果机子上没有gcc，可以安装一个Dev_c++,在Dev_c++的bin目录下有gcc4.查看环境变量是否设置成功5.最后双击xspin525.tcl，即可启动spin第5章协议验证技术10Windows下安装第5章协议验证技术11RDT1.0(理想状态下数据链路层协议)验证等待来自上层的调用rdt_send(data)packet=make_pkt(data)udt_send(packet)等待来自上层的调用rdt_rcv(packet)Extract(packet,data)deliver_data(data)A)RDT1.0发送端B)RDT1.0接收端理想状态下，信道无误码，不丢失报文，接收方有无限接收能力。第5章协议验证技术12RDT1.0验证第5章协议验证技术13RDT2.0验证等待来自上层的调用等待ACK或NAKrdt_rcv(rcvpkt)&&isACK(rcvpkt)rdt_send(data)sndpkt=make_pkt(data,checksum)udt_send(sndpkt)udt_send(sndpkt)rdt_rcv(rcvpkt)&&isNAK(rcvpkt)A)RDT2.0发送端等待来自下层的调用rdt_rcv(rcvpkt)&&corrupt(rcvpkt)sndpkt=make_pkt(NAK)udt_send(sndpkt)rdt_rcv(rcvpkt)&¬corrupt(rcvpkt)extract(rcvpkt,data)deliver_data(data)sndpkt=make_pkt(ACK)udt_send(sndpkt)B)RDT2.0接收端报文出错但不丢失，应答帧不出错也不丢失，接收方没有无限接收能力。第5章协议验证技术14RDT2.0验证一般性验证结果第5章协议验证技术15RDT2.0验证RDT2.0无进展循环验证结果第5章协议验证技术16RDT3.0验证等待来自上层的调用0等待ACK0等待ACK1等待来自上层的调用1rdt_send(data)sndpkt=make_pkt(0，data,checksum)udt_send(sndpkt)start_timerrdt_rcv(rcvpkt)&&(corrupt(rcvpkt)||isACK(rcvpkt,1))timeoutudt_send(sndpkt)start_timerrdt_rcv(rcvpkt)&¬corrupt(rcvpkt)&&isACK(rcvpkt,0)stop_timerrdt_rcv(rcvpkt)rdt_send(data)sndpkt=make_pkt(1，data,checksum)udt_send(sndpkt)start_timerrdt_rcv(rcvpkt)&&(corrupt(rcvpkt)||isACK(rcvpkt,0))udt_send(sndpkt)start_timertimeoutrdt_rcv(rcvpkt)&¬corrupt(rcvpkt)&&isACK(rcvpkt,1)stop_timerrdt_rcv(rcvpkt)报文应答均会出错，但不丢失，接收方没有无限接收能力。第5章协议验证技术17RDT3.0验证RDT3.0一般性验证结果第5章协议验证技术18RDT3.0验证RDT3.0无进展循环验证结果第5章协议验证技术19实验题目题目：6-6(A-B协议)或6-7(GO-BACK-N协议)要求：代码整理成一个目录，目录名为“学号姓名”，压缩后发到我的邮箱[e-mail]，同时在邮件中注明自己的学号和姓名1.提交协议验证的代码2.撰写实验报告•协议验证的设计思路•验证的结果•存在的问题截止时间：2015年12月6日