第6章-协议验证工具解说.ppt

第5章 协议验证技术 第 6 章 协议验证工具 * 内容提要 SPIN概述 1 PROMELA语言 2 SPIN应用 3 * SPIN SPIN（Simple Promela Interpreter）是一种适用于分布式软件系统的形式化验证的开源软件工具：用C语言开发的模型检查工具 SPIN的开发者Gerard J. Holzmann获得了ACM 2001年度软件系统奖(Software Systems Award) * SPIN SPIN特点 SPIN对用Promela语言描述的网络协议设计规格说明（Specification）的逻辑一致性进行检验，并报告系统中出现的死锁、无效的循环、未定义的接收和标记不完全等情况 SPIN无需构建一个全局的状态图，而可以根据需要生成系统自动机的部分状态进行检验（on-the-fly技术） SPIN支持同步和异步两种通信方式 对于给定的一个使用PROLEMA描述的协议系统，SPIN可以对其执行任意的模拟，也可以生成一个C代码程序，然后对该系统的正确性进行有效的检验 适于不同规模的系统的验证 * 内容提要 SPIN概述 1 PROMELA语言 2 SPIN应用 3 * PROMELA语言 在SPIN中，将描述协议实体间所有交互过程的协议描述称为验证模型（validation model），而将描述验证模型的语言称为PROMELA (Protocol/Process Meta Language) PROMELA是一种类似于C程序设计语言的形式描述语言，它可以方便地描述形式化验证模型中的系统的各种行为。 一个用PROMELA描述的协议验证模型由三类对象构成： 进程（processes）、报文通道（message channels）、状态变量（state variables） 所有进程被定义为全局对象，而报文通道和状态变量则是进程使用的全局或局部数据。 实际上，验证模型相当于一个前面所述的有限状态机 详细内容见本书第六章 * 内容提要 SPIN概述 1 PROMELA语言 2 SPIN应用 3 * SPIN安装 Spin验证器有两种版本：windows版和Linux版，且两个版本均有相应的图形框架支持，前者使用jspin或xspin，后者使用ispin实现。 jSpin采用基于java开发的可视化框架，可直接运行于windows平台，但其没有图形化的仿真工具，无法直观看到协议运行的过程。 XSpin运行于Cygwin平台上，利用类UNIX的命令行方式启动。Xspin启动成功后仍然可以使用图形化的操作方式。 * Windows下安装 1.下载相关软件：spin,Xspin,和tcl,，其中tcl区分64位和32位，下载时注意区别，下载的软件是：xspin430.tcl，pc_spin430, ActiveTcl.295590-win32-ix86-threaded.exe tcl下载地址：/activetcl， spin下载地址：/spin/Src/index.html。 2.安装ActiveTcl.295590-win32-ix86-threaded.exe 3.配置环境变量 首先将下载的spin加入PATH路径 再将gcc编译器写入PATH，如果机子上没有gcc，可以安装一个Dev_c++,在Dev_c++的bin目录下有gcc 4.查看环境变量是否设置成功 5.最后双击xspin525.tcl，即可启动spin * Windows下安装 * RDT1.0 (理想状态下数据链路层协议) 验证 理想状态下，信道无误码，不丢失报文，接收方有无限接收能力。 * RDT1.0验证 * RDT2.0 验证 报文出错但不丢失，应答帧不出错也不丢失，接收方没有无限接收能力。 * RDT2.0 验证 一般性验证结果 * RDT2.0 验证 RDT2.0无进展循环验证结果 * RDT3.0 验证 报文应答均会出错，但不丢失，接收方没有无限接收能力。 * RDT3.0验证 RDT3.0一般性验证结果 * RDT3.0验证 RDT3.0无进展循环验证结果 * 实验题目 题目：6-6 (A-B协议) 或 6-7(GO-BACK-N协议) 要求：代码整理成一个目录，目录名为“学号姓名”，压缩后发到我的邮箱 xdsjf@163.com，同时在邮件中注明自己的学号和姓名 1.提交协议验证的代码 2.撰写实验报告 协议验证的设计思路 验证的结果 存在的问题 截止时间：2015年12月6日 * * * * /*-------------------------------RDT1.0 Promela 语言描述-----------------------------------*/ #define M