两本模型检测工具spin的经典之作

razor-

SPIN（Simple Promela Interpreter）是适合于并行系统，尤其是协议一致性的辅助分析检测工具，由贝尔实验室的形式化方法与验证小组于1980年开始开发的pan就是现在SPIN的前身。1989年SPIN的0版本推出主要用于检测一系列的ω-regular属性。1995年偏序简约和线性时序逻辑转换的引入使得SPIN的功能进一步扩大。2001年推出的SPIN4.0版本支持C代码的植入，应用的灵活性进一步增强。在随后2003年推出的SPIN4.1版本加入了深度优先搜索算法，更是使得SPIN的发展上了一个新台阶[http://www.spinroot.com/spin/Doc/course/]。

NASA 使用SPIN检测早在1996年火星探测者所存在的错误，结果发现一些错误是可以在发射之前就可以被改正的。SPIN从此就被用来检测土星火箭控制软件和一些应用与外层空间的程序。

Lucent公司也发现了SPIN 的优点，PathStar Access Server是受益于Holzmann（SPIN开发者）的工作的第一个Lucent产品，Holzmann用SPIN 检测了5ESS Switch的新版本代码，这个软件现在用于Lucent的灵活性部分来改善软件测试的过程。

SPIN良好的算法设计和非凡的检测能力得到了ACM(Association for Computing Machinery)（世界最早的专业计算机协会）的认可，在2001年授予SPIN的开发者Holzmann享有声望的软件系统奖[获奖名单http://www.acm.org/awards/ssaward.html]（Software Systems Award）（其它获得该奖的还有Unix，TCP/IP，Tcl/Tk，Java，WWW等）。Holzmann由此成为继Ken Thompson and Dennis Ritchie（UNIX的开发者）和John M.Chambers（S系统的开发者）之后又一个获得此项殊荣的贝尔人。迄今为止SPIN也是唯一获得ACM软件系统奖的模型检测工具[Gerard J. Holzmann 所获奖项 http://spinroot.com/gerard/]。

2002年4月份在多伦多颁发此奖时，提名表扬SPIN为：“使用先进的理论的验证方法可以被用于大型的和高度复杂的软件系统中”。ACM的CEO John R. White 说道：“Gerard Holzmann的SPIN系统有着非常聪明的查找技术，因为它不但可以在有限的内存空间中快速的对软件进行检测，而且它可以保证程序在按照它们原有的工作方式下被检测。”SPIN是针对软件的检测工具，它是用ANSI C开发的，可以在所有UNIX操作系统版本使用，也可以在安装了Linux、Windows95以上版本等操作系统中使用。在使用SPIN软件进行检测时，系统还要安装ANSI C 编译软件。 在众多的模型检查工具中选用SPIN的理由如下：• perhaps better to understand one systemreally well, than understanding many different systems only in part• spin is free, well-documented, activelymaintained, and has a large and rapidly growing user-base• spin is targets software (not hardware)verification • based on a well-understood theory ofω-automata and temporal logic• the only model checker to have won the ACMSoftware Systems Award so far (other winners include: Unix, TCP/IP, Tcl/Tk,Java)• international Spin user workshops are heldyearly• Italy 1999, Netherlands 1997, France 1998,2002, Canada 1995, 2002, USA 1996, 2000, 2003• 11th Spin workshop: Spain, Barcelona, 1-3 April 2004

359705716

thanks

andrew97

谢谢！

myhz

thanks!

tlhuang168

thanks

modelsim64

谢谢!!

protea_ban

太感谢了这spin的教程太少了