协议验证工具课件.pptVIP

第6章协议验证工具

SPIN概述123PROMELA语言SPIN应用2

vSPIN（SimplePromelaInterpreter）是一种适用于分布式软件系统的形式化验证的开源软件工具：用C语言开发的模型检查工具vSPIN的开发者GerardJ.Holzmann获得了ACM2001年度软件系统奖(SoftwareSystemsAward)3

vSPIN特点?SPIN对用Promela语言描述的网络协议设计规格说明（Specification）的逻辑一致性进行检验，并报告系统中出现的死锁、无效的循环、未定义的接收和标记不完全等情况?SPIN无需构建一个全局的状态图，而可以根据需要生成系统自动机的部分状态进行检验（on-the-fly技术）?SPIN支持同步和异步两种通信方式?对于给定的一个使用PROLEMA描述的协议系统，SPIN可以对其执行任意的模拟，也可以生成一个C代码程序，然后对该系统的正确性进行有效的检验?适于不同规模的系统的验证4

SPIN概述123PROMELA语言SPIN应用5

v在SPIN中，将描述协议实体间所有交互过程的协议描述称为验证模型（validationmodel），而将描述验证模型的语言称为PROMELA(Protocol/ProcessMetaLanguage)vPROMELA是一种类似于C程序设计语言的形式描述语言，它可以方便地描述形式化验证模型中的系统的各种行为。v一个用PROMELA描述的协议验证模型由三类对象构成：?进程（processes）、报文通道（messagechannels）、状态变量（statevariables）?所有进程被定义为全局对象，而报文通道和状态变量则是进程使用的全局或局部数据。?实际上，验证模型相当于一个前面所述的有限状态机v详细内容见本书第六章6

SPIN概述123PROMELA语言SPIN应用7

vSpin验证器有两种版本：windows版和Linux版，且两个版本均有相应的图形框架支持，前者使用jspin或xspin，后者使用ispin实现。?jSpin采用基于java开发的可视化框架，可直接运行于windows平台，但其没有图形化的仿真工具，无法直观看到协议运行的过程。?XSpin运行于Cygwin平台上，利用类UNIX的命令行方式启动。Xspin启动成功后仍然可以使用图形化的操作方式。8

v1.下载相关软件：spin,Xspin,和tcl,，其中tcl区分64位和32位，下载时注意区别，下载的软件是：xspin430.tcl，?tcl下载地址：，?spin下载地址：/spin/Src/index.html。v2.安装v3.配置环境变量?首先将下载的spin加入PATH路径?再将gcc编译器写入PATH，如果机子上没有gcc，可以安装一个Dev_c++,在Dev_c++的bin目录下有gccv4.查看环境变量是否设置成功v5.最后双击xspin525.tcl，即可启动spin9

10

理想状态下，信道无误码，不丢失报文，接收方有无限接收能力。11

12

报文出错但不丢失，应答帧不出错也不丢失，接收方没有无限接收能力。13

一般性验证结果14

RDT2.0无进展循环验证结果15

报文应答均会出错，但不丢失，接收方没有无限接收能力。16

RDT3.0一般性验证结果17

RDT3.0无进展循环验证结果18

u题目：6-6(A-B协议)或6-7(GO-BACK-N协议)u要求：代码整理成一个目录，目录名为“学号姓名”，压缩后发到我的邮箱，同时在邮件中注明自己的学号和姓名?1.提交协议验证的代码?2.撰写实验报告?协议验证的设计思路?验证的结果?存在的问题u截止时间：2015年12月6日19