spin安装及模型验证实验报告

《spin安装及模型验证实验报告》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、实验报告实验题目：基于SPIN的LTL模型检测课程名：形式化方法姓名：王燕霞学号：201428013229141—、SPIN概述SPIN是由贝尔实验室形式化方法与验证小组用ANSIC开发，可以在所有UNIX操作系统版本使用，也可以在安装了Linux、Windows95以上版本等操作系统中使用，适合于分布式并发系统，尤其是协议一致性的辅助分析检测工具。SPIN模型检验工具的基本思想是求两种自动机所接受语言的交集，若交集为空集，则安全特性得到验证，否则输出不满足安全特性的行为迹。SPIN可以用于以下三

2、种基础模型中：1）作为一个模拟器，允许快速对建立的系统模型进行随意的、引导性的或交互的仿真。2）可以作为一个详尽的分析器，严格的证明用户提出的正确性要求是否满足（使用偏序简约进行最优化检索）。3）用于大型系统近似性证明，用SPIN可以对大型的协议系统进行有效的正确性分析，即使这个系统覆盖了最大限度的状态空间。二、SPIN的安装2.1安装CygwinCygwin是一个在windows平台上运行的类UNIX模拟环境，我们町以通过这个软件在windows系统上模拟简单的unix环境。（1）首先从官网ht

3、tp:〃A/A/w.cvgwin.com/,下载Cygwin女•装包，选择64位windows系统（2）打开软件安装包setup-x86_64.exe,界面如下：2014/11/171匡setup-x86_64,exeCygwinNetReleaseSetupProgramgpoograp4uted*orthe穴2rwtdtalon0theWtWDHHWtMM<1MWut8nwnortwfCuwed•MztApMjarringawviet*aneeyctoupueaWeorV>roUieb«M

4、MtcfbyMaJlYouoenrfwwywi-pgrtde0AOM0MmS«tup.(3)选择installfromInternet,下―步CygwinSetup・ChooseInstallationTypeChooseADownloadSourceChoosewhethertoratalordownloadfromthertemet.orrutalfromftesinalocaldrectocy•Irwtalf

5、romHemet如fies*bekeptfcx©um)Q)DownloadWthoUkwtaftngOFalfromLocalOrectory<上FB)下TWN)>（4）选择安装路径(5)选择模拟的Unix环境在系统中的路径匚CygwinSetup-SelectLocalPackageDirectorySelectLocalPackageDerectocySetodadrectorywhereyouwvtSetuptostoretheratalabonfiestdowrioahThedredoty

6、becreateditdoesnotsteadye»Acm32LocalPackageDrectoryBrowse<±-tf(B)T-Jf(N)二KMi(6)选择UseInternetExplorerProxySetting,根据自己的网络链接状态选择（7）选择镜像，最好是选国内的，以.5结尾或者含有.5的，国外镜像下载速度只有几K,所以可以不用尝试。在这里我选择的是屮科人的一个镜像http://mirrors.ustc.edu.cn（8）选择要安装的包,Cygwin默认安装的东西很少,像gcc、

7、make、XII、tcl/TK这些都没有,需要白己勾选，可以在Search-）■直接输入关键字进行查找。如果一次安装没有全都装上也不要紧，可以再次运行setup.exe,然后继续安装其他的包。L（9）点击下一步，等待安装完毕。ProgressThispagedisplaystheprogressofthedownloadornstalabon.Downloadng..2.2在Cygwin中安装yacc和SPINo(1)第一步，编译YACC先卜载ftp://ftp.cs.berkeley.edu/u

8、cb/4bsd/byacc.tanZ用编译yacc.exe：将byacc.tar.Z放在一个空目录yacc中,解压:gunzip*.tar.Z;tar-xf*.tar;然后用make编译,若有错误再用下面命令编译:gcc-oyacc*.o将yacc.exe拷贝到cygwin/bin下(或Src*目录下)(2)第二步，编译SPIN在SPIN官网http://spinroot.com/spin/Src/index.html上卜载spin642.tar.gz放在一个空目录spin中，解压