第6章-协议验证工具

1、第第 6 章章 协议验证工具协议验证工具第第5章章 协议验证技术协议验证技术 2内容提要内容提要SPIN概述概述1PROMELA语言语言2SPIN应用应用3第第5章章 协议验证技术协议验证技术 3SPINvSPIN（Simple Promela Interpreter）是一种适用于）是一种适用于分布式软件系统的形式化验证的开源软件工具：分布式软件系统的形式化验证的开源软件工具：用用C语言开发的模型检查工具语言开发的模型检查工具vSPIN的开发者的开发者Gerard J. Holzmann获得了获得了ACM 2001年度软件系统奖年度软件系统奖(Software Systems Award)第第

2、5章章 协议验证技术协议验证技术 4SPINvSPIN特点特点 SPIN对用对用Promela语言描述的网络协议设计规格说明语言描述的网络协议设计规格说明（Specification）的逻辑一致性进行检验，并报告系统中出现的死）的逻辑一致性进行检验，并报告系统中出现的死锁、无效的循环、未定义的接收和标记不完全等情况锁、无效的循环、未定义的接收和标记不完全等情况 SPIN无需构建一个全局的状态图，而可以根据需要生成系统自动无需构建一个全局的状态图，而可以根据需要生成系统自动机的部分状态进行检验（机的部分状态进行检验（on-the-fly技术）技术） SPIN支持同步和异步两种通信方式支持同步和异

3、步两种通信方式 对于给定的一个使用对于给定的一个使用PROLEMA描述的协议系统，描述的协议系统，SPIN可以对其可以对其执行任意的模拟，也可以生成一个执行任意的模拟，也可以生成一个C代码程序，然后对该系统的代码程序，然后对该系统的正确性进行有效的检验正确性进行有效的检验 适于不同规模的系统的验证适于不同规模的系统的验证第第5章章 协议验证技术协议验证技术 5内容提要内容提要SPIN概述概述1PROMELA语言语言2SPIN应用应用3第第5章章 协议验证技术协议验证技术 6PROMELA语言语言v 在在SPIN中，将描述协议实体间所有交互过程的协议描述称为验证模型中，将描述协议实体间所有交互过

4、程的协议描述称为验证模型（validation model），而将描述验证模型的语言称为），而将描述验证模型的语言称为PROMELA (Protocol/Process Meta Language) v PROMELA是一种类似于是一种类似于C程序设计语言的形式描述语言，程序设计语言的形式描述语言，它可以方便地描述形式化验证模型中的系统的各种行为。它可以方便地描述形式化验证模型中的系统的各种行为。v 一个用一个用PROMELA描述的协议验证模型由三类对象构成：描述的协议验证模型由三类对象构成： 进程（进程（processes）、报文通道（）、报文通道（message channels）、状态变

5、量）、状态变量（state variables） 所有进程被定义为全局对象，而报文通道和状态变量则是进程使用所有进程被定义为全局对象，而报文通道和状态变量则是进程使用的全局或局部数据。的全局或局部数据。 实际上，验证模型相当于一个前面所述的有限状态机实际上，验证模型相当于一个前面所述的有限状态机 v 详细内容见本书第六章详细内容见本书第六章第第5章章 协议验证技术协议验证技术 7内容提要内容提要SPIN概述概述1PROMELA语言语言2SPIN应用应用3第第5章章 协议验证技术协议验证技术 8SPIN安装安装vSpin验证器有两种版本：验证器有两种版本：windows版和版和Linux版，且版

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

7、术协议验证技术 9Windows下安装下安装v 1.下载相关软件：下载相关软件：spin,Xspin,和和tcl,，其中，其中tcl区分区分64位和位和32位，下载时注意区别，下载的软件是：位，下载时注意区别，下载的软件是：xspin430.tcl，pc_spin430, ActiveTcl.295590-win32-ix86-threaded.exe tcl下载地址：下载地址：http:/ spin下载地址：下载地址：http:/ 2.安装安装ActiveTcl.295590-win32-ix86-threaded.exev 3.配置环境变量配置环境变量 首先

8、将下载的首先将下载的spin加入加入PATH路径路径 再将再将gcc编译器写入编译器写入PATH，如果机子上没有，如果机子上没有gcc，可以安装一个，可以安装一个Dev_c+,在在Dev_c+的的bin目录下有目录下有gccv 4.查看环境变量是否设置成功查看环境变量是否设置成功v 5.最后双击最后双击xspin525.tcl，即可启动，即可启动spin第第5章章 协议验证技术协议验证技术 10Windows下安装下安装第第5章章 协议验证技术协议验证技术 11RDT1.0 (理想状态下数据链路层协议理想状态下数据链路层协议) 验证验证等待来自上等待来自上层的调用层的调用rdt_send(da

9、ta)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 验证验证等待来等待来自上层自上层的调用的调用等待等待ACKACK或或NAKNAKrdt_rcv(rcvpkt) & isACK(rcvpkt

10、)rdt_send(data)sndpkt = make_pkt(data, checksum)udt_send(sndpkt)udt_send(sndpkt)rdt_rcv(rcvpkt) & isNAK(rcvpkt)A A) )RDT RDT 2 2. .0 0 发送端发送端等待来自等待来自下层的调下层的调用用rdt_rcv(rcvpkt) & corrupt(rcvpkt)sndpkt = make_pkt(NAK)udt_send(sndpkt)rdt_rcv(rcvpkt) & notcorrupt(rcvpkt)extract(rcvpkt, data)d

11、eliver_data(data)sndpkt = make_pkt(ACK)udt_send(sndpkt)B B) )RDT RDT 2 2. .0 0 接收端接收端报文出错但不丢失，应答帧不出错也不丢失，接收方没有无限接收能力。第第5章章 协议验证技术协议验证技术 14RDT2.0 验证验证一般性验证结果第第5章章 协议验证技术协议验证技术 15RDT2.0 验证验证RDT2.0无进展循环验证结果 第第5章章 协议验证技术协议验证技术 16RDT3.0 验证验证等待来自上等待来自上层的调用层的调用0 0等待等待ACKACK0 0等待等待ACKACK1 1等待来自上等待来自上层的调用层的调

12、用1 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) & notcorrupt(rcvpkt) & isACK(rcvpkt, 0)stop_timerrdt_rcv(rcvpkt)rdt_send(data)sndpkt = make_pkt(1，data, c

13、hecksum)udt_send(sndpkt)start_timerrdt_rcv(rcvpkt) & (corrupt(rcvpkt) | isACK(rcvpkt, 0)udt_send(sndpkt)start_timertimeoutrdt_rcv(rcvpkt) & notcorrupt(rcvpkt) & isACK(rcvpkt, 1)stop_timerrdt_rcv(rcvpkt)报文应答均会出错，但不丢失，接收方没有无限接收能力。第第5章章 协议验证技术协议验证技术 17RDT3.0验证验证RDT3.0一般性验证结果第第5章章 协议验证技术协议验证技术 18RDT3.0验证验证RDT3.0无进展循环验证结果第第5章章 协议验证技术协议验证技术 19实验题目实验题目u题目：题目：6-6 (A-B协议协议) 或或 6-7(GO-BA