并发系统的promela语言建模与spin模型检测

《并发系统的promela语言建模与spin模型检测》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、计算机研究生开放研究《并发系统的Promela语言建模与SPIN模型检测》001模型检测工具SPIN安装使用002SPIN的建模语言Promela003Promela语言建模示例004时序逻辑LTL与CTL0050电梯协议的Promela建模与Spin检测分析005AB协议SPIN的检测分析006克莱顿隧道协议形式化分析0071密码协议的Promela建模与Spin检测分析10072密码协议的Promela建模与Spin检测分析20073密码协议的Promela建模与Spin检测分析30081Petri网的Promela建模与SPIN检验10082Petri网的Promela建模与SPIN检验

2、20083Petri网的Promela建模与SPIN检验30084Petri网的Promela建模与SPIN检验40091论文、研究课题与参考资料1自动模型检测—模型检测工具SPIN安装使用1SPIN概述1．1SPIN的历史背景SPIN（SimplePromelaInterpreter）是适合于并行系统，尤其是协议一致性的辅助分析检测工具，由贝尔实验室的形式化方法与验证小组于1980年开始开发的pan就是现在SPIN的前身。1989年SPIN的0版本推出主要用于检测一系列的ω-regular属性。1995年偏序简约和线性时序逻辑转换的引入使得SPIN的功能进一步扩大。2001年推出的SPIN4

3、.0版本支持C代码的植入，应用的灵活性进一步增强。在随后2003年推出的SPIN4.1版本加入了深度优先搜索算法，更是使得SPIN的发展上了一个新台阶[http://www.spinroot.com/spin/Doc/course/]。NASA使用SPIN检测早在1996年火星探测者所存在的错误，结果发现一些错误是可以在发射之前就可以被改正的。SPIN从此就被用来检测土星火箭控制软件和一些应用与外层空间的程序。Lucent公司也发现了SPIN的优点，PathStarAccessServer是受益于Holzmann（SPIN开发者）的工作的第一个Lucent产品，Holzmann用SPIN检测了

4、5ESSSwitch的新版本代码，这个软件现在用于Lucent的灵活性部分来改善软件测试的过程。SPIN良好的算法设计和非凡的检测能力得到了ACM(AssociationforComputingMachinery)（世界最早的专业计算机协会）的认可，在2001年授予SPIN的开发者Holzmann享有声望的软件系统奖[获奖名单http://www.acm.org/awards/ssaward.html]（SoftwareSystemsAward）（其它获得该奖的还有Unix，TCP/IP，Tcl/Tk，Java，WWW等）。Holzmann由此成为继KenThompsonandDennisRi

5、tchie（UNIX的开发者）和JohnM.Chambers（S系统的开发者）之后又一个获得此项殊荣的贝尔人。迄今为止SPIN也是唯一获得ACM软件系统奖的模型检测工具[GerardJ.Holzmann所获奖项http://spinroot.com/gerard/]。2002年4月份在多伦多颁发此奖时，提名表扬SPIN为：“使用先进的理论的验证方法可以被用于大型的和高度复杂的软件系统中”。ACM的CEOJohnR.White说道：“GerardHolzmann的SPIN系统有着非常聪明的查找技术，因为它不但可以在有限的内存空间中快速的对软件进行检测，而且它可以保证程序在按照它们原有的工作方式下

6、被检测。”SPIN是针对软件的检测工具，它是用ANSIC开发的，可以在所有UNIX操作系统版本使用，也可以在安装了Linux、Windows95以上版本等操作系统中使用。在使用SPIN软件进行检测时，系统还要安装ANSIC编译软件。在众多的模型检查工具中选用SPIN的理由如下：•perhapsbettertounderstandonesystemreallywell,thanunderstandingmanydifferentsystemsonlyinpart•spinisfree,well-documented,activelymaintained,andhasalargeandrapidl

7、ygrowinguser-base•spinistargetssoftware(nothardware)verification•basedonawell-understoodtheoryofω-automataandtemporallogic•theonlymodelcheckertohavewontheACMSoftwareSystemsAwardsofar(otherwinnersinclu