spin安装模型验证实验报告.docx

实验报告 实验题目：基于SPIN的LTL模型检测 课 程 名： 形式化方法 姓 名： 王燕霞 学 号： 201428013229141 一、SPIN?概述 SPIN是由贝尔实验室形式化方法与验证小组用ANSI C开发，可以在所有UNIX操作系统版本使用，也可以在安装了Linux、Windows95以上版本等操作系统中使用，适合于分布式并发系统，尤其是协议一致性的辅助分析检测工具。 SPIN模型检验工具的基本思想是求两种自动机所接受语言的交集，若交集为空集，则安全特性得到验证，否则输出不满足安全特性的行为迹。 SPIN可以用于以下三种基础模型中： 1）?作为一个模拟器，允许快速对建立的系统模型进行随意的、引导性的或交互的仿真。 2）?可以作为一个详尽的分析器，严格的证明用户提出的正确性要求是否满足（使用偏序简约进行最优化检索）。 3）?用于大型系统近似性证明，用SPIN可以对大型的协议系统进行有效??正确性分析，即使这个系统覆盖了最大限度的状态空间。 二、SPIN的安装 2.1安装Cygwin Cygwin是一个在windows平台上运行的类UNIX模拟环境，我们可以通过这个软件在windows系统上模拟简单的unix环境。 首先从官网 HYPERLINK / /，下载Cygwin安装包，选择64位windows系统 打开软件安装包setup-x86_64.exe，界面如下： 选择install from Internet，下一步 选择安装路径 选择模拟的Unix环境在系统中的路径 选择Use Internet Explorer Proxy Setting，根据自己的网络链接状态选择 选择镜像，最好是选国内的，以.cn结尾或者含有.cn的，国外镜像下载速度只有几K，所以可以不用尝试。在这里我选择的是中科大的一个镜像 HYPERLINK  (8)选择要安装的包，Cygwin默认安装的东西很少，像gcc、make、X11、tcl/TK这些都没有，需要自己勾选，可以在Search中直接输入关键字进行查找。如果一次安装没有全都装上也不要紧，可以再次运行setup.exe，然后继续安装其他的包。 （9）点击下一步，等待安装完毕。 2.2在Cygwin中安装yacc和SPIN。 （1）第一步，编译YACC 先下载 /ucb/4bsd/byacc.tar.Z 用编译yacc.exe： 将byacc.tar.Z放在一个空目录yacc中，解压：gunzip *.tar.Z ; tar -xf *.tar;然后用make编译，若有错误再用下面命令编译： gcc -o yacc *.o将yacc.exe拷贝到cygwin/bin下（或Src*目录下） （2）第二步，编译SPIN 在SPIN官网 HYPERLINK /spin/Src/index.html /spin/Src/index.html 上下载spin642.tar.gz 放在一个空目录spin中，解压：gunzip *.tar.gz; tar -xf *.tar; 转到Src*目录下 cd Src*，make -f make_unix ，最后将生成的spin.exe放到cygwin/bin下。编译好以后的截图如下： （3）这时候运行在Cygwin命令行中输入spin就会显示spin的版本，截图如下： 2.3安装SPIN 的图形界面工具ispin （1）安装ISPIN的前提是Cygwin支持图形界面，也就是刚才我们在安装Cygwin的时候必修安装Tcl/TK和X11，安装好以后在windows开始菜单会出现一个Cygwin-X目录，如下图所示： （2）从SPIN官网 HYPERLINK /spin/Src/index.html%20上下载ispin.tcl /spin/Src/index.html 上下载ispin.tcl放到C:\cygwin64\bin目录下，把后缀去掉，重命名为ispin。 （3）打开Cygwin-X目录下的XWin Server，在命令框中输入ispin就会出现ispin的界面。 （4）遇到的问题： 在这里不知道为什么，大多数同学都没有出现ispin界面错位的问题，但是我的ispin超出了界面，影响到了正常使用。后来在ispin.tcl文件中加了一条关于字体大小的全局声明就好了，经试验对于xspin方法也是一样的。 下面的改代码前后改代码后的界面对比： 三、利用SPIN进行模型检测 3.1互斥协议的模型检测 byte sem = 1; //占用信号：0 表示临界区被占用 byte critical = 0; //临界区