《网络分析与协议测试》实验指导书
郑啸编写
安徽工业大学计算机学院
2008年9月
引言
本门课程的实验工具为SMV，它是卡内基梅隆大学计算机学院开发的模型检验工具软件。

SMV是国际上广为流行的分析有限状态系统的常用工具。

它具有一套用于描述有限状态并发系统的规范语言，为了使用SMV对系统进行检验，首先要使用该规范语言来对系统进行描述（系统说明），并用CTL表示出系统将被检验的属性或性质，然后提交给SMV系统运行。

SMV系统接收了用户提交的输入后，先从系统规范中提取以有序二叉决策图（OBDD）形式表示的迁移系统，然后用基于OBDD的搜索算法确定系统是否满足用CTL描述的被检验性质，最后给出True或False的结果，并在某性质为False的情况下给出导致该结果的反例。

SMV的工作原理如下图所示。

图SMV 工作原理
通过该实验可以使学生掌握用模型检测工具分析简单协议的基本方法，辅助加强学生对协议开发原理的理解和掌握。

一、实验项目
1．实验一SMV模型检测工具的使用
实验目的：熟悉SMV语言的语法和词法。

实验内容：1. 翻译SMV使用指南《The SMV system for SMV version 2.54》（见附录）
2. SMV 程序的使用。

学时：2学时
2．实验二哲学家问题的建模与分析
问题描述：有五位哲学家围绕着餐桌坐，每一位哲学家要么思考要么等待，要么吃饭。

为了吃饭，哲学家必须拿起两双筷子（分别放于左右两端）不幸的是，筷子的数量和哲学家相等，所以每只筷子必须由两位哲学家共享。

为了防止死锁，要设置一些规则，请描述你的协议，并验证。

实验目的：掌握并发程序的建模和分析方法
实验内容：1. 用自然语言描述哲学家进餐问题的内容
2．用有限状态机建模
3．用SMV语言描述
4．验证有关的属性
学时：4学时
3．实验三AB协议的建模与分析
问题描述：AB(Alternating Bit Protocol)协议具有重发机制，并且在应答时附加了“0”和“1”的序号控制。

在该协议中，发送端S交替向接收端R发送序号为“0”和“1”的报文，R交替地回答认可序号为“0”和“1”的认可报文。

实验目的：掌握网络协议的建模和分析方法
实验内容：1. 用自然语言描述协议的内容
2．用有限状态机建模
3．用SMV语言描述
4．验证有关的属性
学时：4学时
二、实验报告书写要求
实验报告应包括：
1．实验目的
2．实验内容
1）协议的有限状态模型
2）协议的SMV语言描述
3）协议的验证属性描述（即SPEC语句）
3．实验结果
程序运行结果，属性是否满足。