自动模型检测—模型检测工具SPIN安装使用 .

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

2、N检测早在1996年火星探测者所存在的错误，结果发现一些错误是可以在发射之前就可以被改正的。SPIN从此就被用来检测土星火箭控制软件和一些应用与外层空间的程序。Lucent公司也发现了SPIN 的优点，PathStar Access Server是受益于Holzmann（SPIN开发者）的工作的第一个Lucent 产品，Holzmann用SPIN 检测了5ESS Switch的新版本代码，这个软件现在用于Lucent的灵活性部分来改善软件测试的过程。SPIN良好的算法设计和非凡的检测能力得到了ACM(Association for Computing Machinery)（世界最早的专业计算机

3、协会）的认可，在2001年授予SPIN的开发者Holzmann享有声望的软件系统奖获奖名单/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 所获奖项 2002年

4、4月份在多伦多颁发此奖时，提名表扬SPIN为：“使用先进的理论的验证方法可以被用于大型的和高度复杂的软件系统中”。 ACM的CEO John R. White 说道：“Gerard Holzmann 的SPIN系统有着非常聪明的查找技术，因为它不但可以在有限的内存空间中快速的对软件进行检测，而且它可以保证程序在按照它们原有的工作方式下被检测。”SPIN是针对软件的检测工具，它是用ANSI C开发的，可以在所有UNIX操作系统版本使用，也可以在安装了Linux、Windows95以上版本等操作系统中使用。在使用SPIN软件进行检测时，系统还要安装ANSI C 编译软件。 在众多的模型检

5、查工具中选用SPIN的理由如下： perhaps better to understand one system really well, than understanding many different systems only in part spin is free, well-documented, actively maintained, and has a large and rapidly growing user-base spin is targets software (not hardware) verification based on a well-understo

6、od theory of -automata and temporal logic the only model checker to have won the ACM Software Systems Award so far (other winners include: Unix, TCP/IP, Tcl/Tk, Java) international Spin user workshops are held yearly Italy 1999, Netherlands 1997, France 1998, 2002, Canada 1995, 2002, USA 1996, 2000,

7、 2003 11th Spin workshop: Spain, Barcelona, 1-3 April 2004 12 SPIN的特征 SPIN验证主要关心的问题是进程之间的信息能否正确的交互，而不是进程内部的具体计算。SPIN是一个基于计算机科学的“形式化方法”，将先进的理论验证方法应用于大型复杂的软件系统当中的模型检测工具6。如今SPIN被广泛的应用于工业界和学术界。其特点如下：1  SPIN以Promela为输入语言，可以对网络协议设计中的规格的逻辑一致性进行检验，并报告系统中出现的死锁、无效的循环、未定义的接收和标记不完全等情况。2  SPI

8、N使用on-the-fly技术，即无需构建一个全局的状态图或者Kripke结构，而可以根据需要生成系统自动机的部分状态。3  SPIN可当做一个完整的LTL（Linear Temporal Logic）模型检验系统来使用，支持所有的可用的线性时态逻辑表示的正确性验证要求，也可以在有效的on-the-fly检验系统中用来检验协议的安全特征。4  SPIN可通过使用会面点来进行同步通信，也可以使用缓冲通道来进行异步通信。5  对于给定的一个使用Promela描述的协议系统，SPIN可以对其执行随意的模拟，也可以生成一个C代码程序，然后对该系统的正确性进行有效的检验。6

9、  在进行检验时，对于中小规模的模型，可以采用穷举状态空间分析，而对于较大规模的系统，则采用Bit State Hashing方法来有选择地搜索部分状态空间。 13 基于SPIN的协议分析 用SPIN对协议进行模拟分析，来确定协议的正确性。正确性是指：不存在违背断言（assertion）的情况、不存在死锁(deadlock)、不存在“坏的”循环、 满足我们定义的LTL公式。在SPIN/Promela模型中主要由：断言（assertion），特殊的标记和never claims三种方式来实现。一个“断言”(assert语句)是一个逻辑表达式。它可以出现在所描述的模型

10、中的任何位置，并在任何时候都是可以执行的。它相当于指定系统的一个“不变式”，无论什么时候这个表达式的值都应为真。在SPIN执行assert语句时，如果该语句所指定的条件成立（表达式的值不为0），则不产生任何影响；但如果条件不成立（表达式的值为0），将产生一个错误报告。在Peomela模型中经常使用assert语句来检验在某状态时某个性质是否成立。死锁（deadlock）是系统运行到某个状态后不能再转向其它任何一个状态。在SPIN验证过程中如果出现死锁情况，验证器将会给出“invalid end state”提示语句。要验证Promela所描述的一个系统是否存在死锁，验证器就要能够将正确的结束状

11、态和异常的结束状态区别开来。在一个执行序列结束时，最好是所有的进程的实例都运行到了其相应进程体的最后，并且所有的消息通道都为空。然而有的时候，并不一定要求所有的进程都到达了它们进程体的最后才能说明不存在死锁，其中有的进程可能会停留在空闲状态，也可能会在某些状态循环，等待某个消息的到来后再进行其他操作。为此，在建模的过程中可以用“end”标记来标识正确的结束状态。一个“坏”的循环是指系统不断重复执行一些错的或是没有意义的行为。建模过程中可以设置“accept”标记（主要用于never 声明中），然后指定验证器找出所有至少执行过一次此标记语句的循环，如果这样的循环不存在则说明系统是正确的。也可以设

12、置“progress”来标记一些必须要不断重复被执行的语句，如果存在没有经过“progress”的循环，则说明有“坏”的循环存在。一个线性时序逻辑公式可以表达比“从不发生”或“总是发生”或“不断的发生”这些属性更复杂的系统要求。比如，系统要求满足 “事件P发生则能得到事件Q也发生了”这个规范约束条件，这时你就可以用线性时序逻辑公式（P->Q）来检测看你的系统是否能够满足这个条件。SPIN 提供了将线性时序逻辑公式翻译为相应的never claims的功能，使用起来相当的方便。 14 SPIN检测的基本过程 SPIN可以用在三个基础模型中SPIN主页1） 作为一个模拟器

13、，允许快速对建立的系统模型进行随意的、引导性的或交互的仿真。2） 可以作为一个详尽的分析器，严格的证明用户提出的正确性要求是否满足（使用偏序简约进行最优化检索）。3） 用于大型系统近似性证明，用SPIN可以对大型的协议系统进行有效的正确性分析，即使这个系统覆盖了最大限度的状态空间。SPIN首先从一个描述的协议系统的高层模型规格开始，经分析没有语法错误后，对系统的交互进行模拟，直到确认系统设计拥有预期的行为；然后，SPIN将产生一个用C语言描述的验证程序，经检验器编译后被执行，执行中如果发现了违背正确性说明的任何反例，则可反馈给交互模拟机，通过重现细节剔除引起错误的原因。图1-1描述了整个的检测

14、过程：   2 SPIN 的安装和使用 21 WIN32环境下SPIN的安装和使用 从可以用spin*.exe在Windows控制台环境下对模型进行相应的检测和错误迹观察了。 22 Java环境下SPIN的安装和使用  上述smv.exe只有控制台界面，以色列的Mordechai (Moti) Ben-Ari使用Java作出了图形界面jSPIN，可如下安装使用: 在Windows2000/NT/XP下 - 使用VC+6.0编译器：先安装并运行成功：VC+6.0、JDK1.5.0将jspin1-1-5.zip解压，得目录/js

15、pin1-1-5，可将此目录放于例如：d:/jspin1-1-5将SPIN4.1.2（Win32版）: pc_spin412.zip解压到后将spin412.exe取出放入d:/jspin1-1-5；打开d:/jspin1-1-5的config文件，做如下改变：设置示例文件所在目录 SOURCE_DIRECTORY=d/:/jspin1-1-5/examples 设置spin412.exe所在目录 SPIN= d/:/jspin1-1-5/spin412.exe 设置VC+6编译命令：C_COMPILER=cl -w -nologo pan.c 鼠标点jSpin.jar运行JSPIN

16、，出现图形界面： JSPIN的图形界面由、工具条和三个窗口组成：菜单栏的formula用来输入对模型性质进行检验的LTL（线性时序逻辑）公式（该公式存盘为扩展名PRP的文件），该公式由工具栏的Translate将其翻译为Promela的never模块并在右窗口显示，同时存盘为扩展名为ltl的文件；右窗口用来录入、编辑模型的Promela程序，并存盘为扩展名为pml的文件（可用菜单的“File”打开）；下窗口是有关操作的记录。 23 一个有问题的互斥协议及其JSPIN检验示例：互斥 - 将下列Promela程序录入，并存盘为sem-error.pml，我们用M表示这个模型&#

17、160;byte sem = 1; /占用信号：0 占用临界区byte critical = 0; /临界区：n 临界区被n人占用#define sss (sem>0)#define mutex (critical <= 1) /要求检验 active proctype P1 () do : atomic sem > 0; sem-; critical+; /进程P1占用临界区critical-; /进程P1退出临界区sem+; /释放占用信号odactive proctype P2 () do : critical+; /进程P2占用临界区critical-; /

18、进程P2退出临界区od 显然，由于并发性，这个系统的模型M不满足：要求临界区不被多于1个用户同时使用，用LTL语言描述这个互斥性质： mutex，使用JSPIN发现错误（即M |/= mutex）：点击工具栏的“Verify”，这时JSPIN首先使用spin生成pan.c等文件，接着自动调用VC+6编译器将pan.c编译为可执行文件pan.exe，在下窗口可见到编译的指令为：cl -w -nologo pan.c DSAFETY o pan pan.c并自动运行pan.exe X进行建议，检验结果在右窗口：出现一个错误“errors: 1”，错误的轨迹存放的文件名 类似地，

19、我们可以对下列LTL公式描述的系统性质进行检验：M |= <>mutex （可能只有一个用户占用临界区）M |/= !<>mutexM |= ! mutex（使用Safety模式）M |/= ! mutex（使用Acceptance模式）M |= <>!mutex（使用Safety模式）M |/= <>!mutex（使用Acceptance模式）M |/= !mutex、M |/= sss -> mutex、M |= !sss -> mutex、 24 正确的协议byte sem = 1;byte critical = 0;

20、#define sss (sem>0)#define mutex (critical <= 1)active proctype P1 () do : atomic sem > 0; sem-; critical+;critical-;sem+;odactive proctype P2 () do : atomic sem > 0; sem-; critical+;critical-;sem+;od 问题与研究 问题：是否在Safety模式不满足，则在Acceptance模式一定不满足？ 问题1：解决中文问题！ 问题2：解决VC+6编译问题！ 如何在Window

21、s2000/NT/XP下 使用Cygwin的gcc编译器 在Cygwin下，要先解决Java1.4的安装运行问题！jSPIN的源代码2.1 研究：如何从源代码编译成软件？2.2 研究：如何进行改造？例如：支持中文？ 3 Cygwin 环境下SPIN的安装和使用先在Windows下安装Cygwin.如果我们只是将刚刚解压得到的spin*.exe，拷贝到cygwin/bin下的话，相当于我们还是在Windows平台操作SPIN，下面我们将给出如何完全的仿真UNIX环境使用SPIN的操作：(以下安装软件，我们已经打包在XSPIN412-Cygwin.rar里，读者可先下载)第一步，先下载

22、/ucb/4bsd/byacc.tar.Z 用编译yacc.exe：将byacc.tar.Z解压： gunzip *.tar.Z tar -xf *.tar然后用make编译，若有错误再用下面命令编译： gcc -o yacc *.o将yacc.exe拷贝到cygwin/bin下（或Src*目录下） 第二步，编译SPIN 1） 在8处下载spin*.tar.gz 放在一个空目录中2) 解压： gunzip *.tar.gz tar -xf *.tar3) 转到Src*目录下cd Src*4) 打开文件make_unix，将第12行等号后的cc命令

23、改为gcc,保存5) make -f make_unix 6) 将生成的spin.exe放到cygwin/bin下，然后参考Test/README.tests进入测试阶段 注：将测试中的cc命令换成gcc命令即可。将cygwin/bin中的cpp.exe拷贝到cygwin/lib下，执行test 1，在第五步和第九步中生成pan.exe，用./pan -l 和./pan -a来验证。 23 SPIN 的图形界面工具XSPIN安装和使用 使用SPIN的最简单的方式是使用图形界面XSPIN，图形界面独立于SPIN 运行，辅助产生和选择相应的SPIN命令，XSPIN在后台运行SP

24、IN得到期望的输出值，XSPIN知道什么时候怎么样去编译模型检测的代码，也知道什么时候如何去执行它。所以可以不用记住所有的参数。下面我们将具体介绍在Cygwin环境下的安装和使用。(1) XSPIN的安装 在 ，将xspin*.tcl改名为xspin拷贝到Cygwin的/bin/下。打开此文件，在文件的前几行你会看到该软件默认执行的路径是 c:/cygwin/bin/xspin 将此项改为你所安装的Cygwin的路径然后保存即可。在/cygwin/bin下找到wish* 文件，改名为wish。现在你就可以将xspin作为标准的UNIX命令使用了，例如：$xspin leader。(2) XSP

25、IN的使用我们用Test文件夹下的leader程序为例说明如何使用XSPIN，具体步骤如下：1 转到Test目录下输入$ xspin leader2 这时你将看到XSPIN的主窗口（如图2- 所示）。整个窗口分四个区域：菜单栏（左上方）。首先点击Help按钮，了解一下相关的帮助主题，阅读完后点击OK返回主窗口。在Edit选项中提供了一些基本的编辑功能和查找功能你可以在文本编辑区用鼠标拖动选择要进行操作的区域，然后用编辑菜单栏的功能进行拷贝剪切和粘贴。右上方提供了显示当前鼠标在文本编辑区中的位置和简单的查找功能。文本编辑区(窗口中间部分)。图中文本编辑区加载了leader election的Pr

26、omela语言的程序说明。日志窗口(主窗口最下面的黑色区域)。它用来显示我们当前使用的SPIN、XSPIN和TclTk的版本号，还有我们运行时所执行的相应的SPIN命令和一些提示性语句。 3 点击RUN按钮，选择Run Syntax Check进行语法检测。4 选择Run Slicing Algorithm进行模型冗余检测。在此次检测中系统会给出那些数据在模型中是没有用的，同时还给你一些改进模型的建议。5 选择set simulation parameters.现在使用默认值，点START按钮，开始第一次的仿真运行。6 这时一系列的新窗口出现：message sequence chart ,v

27、ariable values和simulation output窗口。刚开始message sequence chart 是空的，它将列出在仿真过程中所有的消息的发送和接收。variable values窗口将列出所有全局变量和全局通道的当前值（也可以在Simulation Options窗口Data Value Panel中选择要在variable values窗口中显示的数据）。simulation output窗口显示所有执行的语句并在左边显示执行的步骤号。它允许单步执行（点击Single Step按钮）或连续执行（点RUN按钮）。7 当运行完，simulation output窗口将显

28、示多少进程被创建，执行的结果如下图所示： 在日志窗口中将包括这些语句：<starting simulation>spin -X -p -v -g -s -r -n1 -j0 pan_inspin -Z pan_in ;# preprocess input<done preprocess><at end of run>上述结果显示了在用XSPIN综合执行仿真的时候所选的参数。用XSPIN的优越性是显而易见的：你不需要记住所有SPIN的参数的意思只需要选择你想要进行的检测参数就可以了。8 再次转到显示leader election 协议的promela 描述窗口

29、。然后在Message Sequence Chart 窗口中在矩形框和箭头上移动鼠标，当鼠标在矩形框上方时，在主窗口中相应的PROMELA语句就会被反显表示出来，而且执行的语句将显示在矩形框中，如果鼠标不在矩形框上方，则矩形框中的数值是仿真时执行的步数这个步数和在Simulation Output窗口中的步数相匹配。再对黄色的矩形块进行同样的操作，观察它们对应的promela语句。9 转到Simulation Output 窗口，按cancel将会关闭所有基于它产生的新的窗口,下次再运行进行仿真时,默认使用的参数选项就是这次仿真所设定的。 接着,选择Set Verification Param

30、eters选项，使用默认的选项参数，点击run按钮运行，注意观察在日志窗口中使用的命令参数。这次产生一个分析器，分析器被编译和执行，结果在Verification Output窗口中显示出来，如果一切正常，在结果中会显示没有错误被发现，如果在运行中，SPIN发现一些给定参数的状态没有正确的达到（或执行）。这些语句将被反显在主窗口中。关闭verification output 窗口 。在这个领导人选举协议中有一个用LTL公式描述的正确性验证:<>oneLeader ,具体描述详见Test文件夹下的leader.ltl 文件。在下面我们将解释如何使用。10 在程序中加入人为的错误ass

31、ert(false)，再重新进行验证，（没有必要保存文件，XSPIN总是运行在它编辑缓冲区中的程序的副本pan_in）这次验证将返回一个错误的序列，同时弹出一个对话框，问你是使用不同的参数再重新运行还是执行guided 仿真。点击Setup Guided Simulation 按钮，这时返回一个仿真参数窗口，但是现在参数已经被改变了（从原来的Random Simulation 改为Guided Simulation）你可以选择要观察的错误迹文件。11 选中Execution Bar Panel 改子选项Time Sequence Panel 为One Window per Process. 来

32、进行于上次不同的仿真。单击Start按钮，然后在Simulation Output 窗口中单击Run按钮，观察错误迹。这次错误迹在assertion的值为假的时候停止而不是在所有进程都到运行到了他们的最后一行。12 执行完后，关闭这些窗口。接下来，选择LTL Property Manager. 选项，默认情况下将读进一个文件名和主程序名相同，扩展名为.ltl的文件。在这个例子中，将打开leader.ltl 将文件的信息加载进来，你也可以输入不同的逻辑公式。让我们来实验一下，点击clear按钮在formula框中输入: p，这个表达式的含义是p永真。单击Generate按钮或者在Formula输

33、入框中键入回车键，never claim窗口中将产生与LTL语法相应的promela语句。13 在Symbol Definitions中增加宏定义p，#define p(nr_leaders=0 | nr_leaders=1)这个定义，单击Generate按钮，在never claim窗口中将产生与LTL语法相应的promela语句，然后单击Run Verification按钮来观察验证结果。 4 SPIN 的使用 41 SPIN运行时参数将协议系统用Promela建模后，SPIN就可以对系统的执行情况进行随机的模拟，也可以生成相应的C程序，并对系统状态空间进行穷举或者部分

34、搜索检验。下面就介绍一些主要用到的参数：1）spin a 这个参数将生成协议分析器。使用该命令后，其输出将被写入一个名为“pan.cbhmt”的C文件集合，将这些文件编译后便可生成分析器，从而对协议进行分析。$ spin -a abp$ wc pan.? 185 471 2887 pan.b 7235 23889 158923 pan.c 484 1597 9907 pan.h 367 1691 12017 pan.m 702 2752 17931 pan.t 8973 30400 201665 total我们可以观察到，上述操作总共生成了五个文件：文件pan.c包含了用来对协议进行分析的大部

35、分C代码； 文件pan.t包含了对协议控制流进行编码的转换矩阵；文件 pan.b 和pan.m 包含了向前和向后转换的C代码；pan.h则是一般的头文件。这些文件可以采用不同的方式进行编译，从而用于不同情况下的协议分析：完全状态空间搜索的分析或Bit State Hashing方法的选择性探测状态空间分析。如果要进行完全状态空间搜索下的分析，可使用下面的命令来编译上述的C程序：$gcc o pan pan.c其可适用于多达100000个状态的系统状态空间。对于较大的系统，进行穷举状态空间时可能会超出计算机的存储容量，这时可以使用Bit State Space的方法，此时则使用下面的命令来编译上

36、述的C程序。$gcc DBITSTATE o pan pan.c编译后便可以键入“$./pan”进行运行了。2）spin s 显示所有的消息发送行为。并注明发送各个消息的进程的id、该发送操作所对应Promela描述中的行号、所发送消息的具体内容，以及接收消息的通道等。例如，$spin s abp7034: proc 1 (sender) line 10 "abp" Send err,0,0 -> queue 1 (out)7038: proc 2 (receiver) line 54 "abp" Send nak,0,0 -> queue

37、2 (out)7042: proc 1 (sender) line 9 "abp" Send mesg,0,0 -> queue 1 (out)7046: proc 2 (receiver) line 48 "abp" Send nak,0,0 -> queue 2 (out)7050: proc 1 (sender) line 10 "abp" Send err,0,0 -> queue 1 (out)7056: proc 2 (receiver) line 54 "abp" Send nak,

38、0,0 -> queue 2 (out)3) spin r 显示所接收的每一个消息。例如，下面使用了-r 和-s的组合，显示了每个消息的发送和接收情况。 $spin -r -s abp4915: proc 1 (sender) line 9 "abp" Send mesg,0,0 -> queue 1 (out)4916: proc 2 (receiver) line 34 "abp" Recv mesg,0,0 <- queue 1 (in)4919: proc 2 (receiver) line 48 "abp"

39、 Send nak,0,0 -> queue 2 (out)4921: proc 1 (sender) line 16 "abp" Recv nak,0,0 <- queue 2 (in)4924: proc 1 (sender) line 10 "abp" Send err,0,0 -> queue 1 (out)4928: proc 2 (receiver) line 54 "abp" Recv err,0,0 <- queue 1 (in) 4)spin p 显示各进程中所执行的每一个语句。例如，$spi

40、n p abp 3697: proc 1 (sender) line 13 "abp" (state 23) (timeout)3698: proc 1 (sender) line 14 "abp" (state 11) goto again3699: proc 1 (sender) line 8 "abp" (state 8) out!mesg,o,s3700: proc 2 (receiver) line 33 "abp" (state 21) in?mesg,i,s3701: proc 1 (sender)

41、line 13 "abp" (state 9) .(goto)3702: proc 2 (receiver) line 35 "abp" (state 17) (s!=es)3703: proc 2 (receiver) line 47 "abp" (state 15) out!err,0,03704: proc 1 (sender) line 13 "abp" (state 23) in?err,0,05)spin l 通常与选项-p结合使用，显示进程的局部变量的当前值。6)spin g 显示全局变量的当前值。7

42、)spin t 一个迹搜索选项。如果分析器发现了死锁、断言不成立或者未指定的接收等情况，它将会将一个错误迹写入文件*.trail中。在调用SPIN时如果加上选项-t，就可以对这些错误进行观察。将选项-t,-p,-g,-l,-s,-r等选项结合使用，便可以对错误序列进行不同的观察。在命令提示符“$”下输入spin -,可以看到所有能使用的SPIN 的参数。 42 pan 运行时参数和编译时参数$./pan l 用来检验系统是否存在没有执行progress语句的循环。这个选项能使用的前提是在生成检验器的时候使用选项-DNP：$gcc DNP o pan pan.c$./pan a 检测含

43、有accept标记语句的循环。$./pan A 忽略对assert()语句的检测。$./pan e 为所有的错误创建错误迹。$./pan E 忽略不正确的结束状态。$./pan n 不列出未达到的状态。在命令提示符“$”下输入./pan -,可以看到所有能使用的pan运行时和编译时参数。更多的参数可以参考：/VirtualHelp/Info/Spin/Pan.html#D0。 43 pan 的输出格式简介 一般典型的验证输出结果如下示： 1 (Spin Version 4.1.2 - 21 February 2004) 2 + Partial Order Reduction3 Full statespace search for: 4 never claim - (none specified) 5 assertion violations + 6 acceptance cycles - (not selected) 7 invalid end states + 8 State-vector 52 byte, depth rea