SPIN模型检测的工作原理

关于自动机及进程及系统方面的免费优秀学术论文范文，自动机方面毕业论文模板,关于SPIN模型检测的工作原理相关论文范文例文，对写作自动机论文范文课题研究的大学硕士、本科毕业论文开题报告范文和文献综述及职称论文参考文献资料下载有帮助。

摘 要：SPIN模型检测主要是用来检测分布式软件系统的,目前被普遍用于庞大而复杂的软件系统验证上.本文主要介绍了SPIN模型检测的发展历程、主要特点、基本结构和工作原理.

关 键 词 ：SPIN；特点；模型检测；工作原理

中图分类号：TP311.52 文献标识码：A 文章编号：1674-7712 （2013） 08-0000-01

一、SPIN的简介

(一)SPIN的发展历程

SPIN是一种用来分析和验证并发系统,在逻辑是否一致的辅助验证器,它主要是针对软件检测,而不是验证硬件是否能高效运行.SPIN从1980年Bell实验室推出的仅对安全性进行验证的Pan验证系统开始着手研究；1983年更名为Trace,这代表SPIN的验证方法有了转变,从过去的使用的进程代数变成使用自动机理论；在1989年终于推出能进行协议验证的第一个版本；1994年又推出了基于Partial-order reduction基础上的静态归纳技术STREM；1995年通过内嵌算法进一步加强了SPIN的功能；1997年发现软件验证新思想,在某些程度上,降低对内存的需求；1993年SPIN3.3采用Statement Merging技术,在降低内存需求的同时大大缩短了验证的时间；2000年引用Property-base Slicing技术到自动模型的抽取中；2001年SPIN4.0中采用能对嵌入的C语言代码进行检测的模型抽取器；紧接着2003年SPIN4.1引进深度优先的搜索算法,让SPI得到突破性的发展.

(二)SPIN的主要特点

进程内部的具体怎么计算SPIN验证并不关心,它所关心的是每个进程间的消息能否准确的交互.SPIN结合先进的理论验证方法,专门对大型且复杂的软件系统进行模型检测,如今SPIN验证被大量用在学术界和工业界.它具有以下的特点：

（1）把Promela作为SPIN的输入语言是,能较好的检验网络协议的一致性,找出系统中存在的无效循环、死锁、未定义的接收以及标记不完整等问题；（2）SPIN采用on-the-fly技术,可以不必搭建一个完整的状态图或Kripke框架,而是由系统自动生成部分状态；（3）SPIN是一个完整的LTL模型检测系统,能验证基本上所有能用的线性时态的逻辑表示是否正确,还能有效地检验协议的安全性；（4）SPIN不仅能进行同步通信,更能采用缓冲通道实现异步通信；（5）一个采用Promela描述的系统,SPIN既能对它实行任意的模拟,也能先生成C语言代码后,再验证系统的正确性；（6）验证过程中,如果是中小型系统,使用穷举状态空间就能进行分析,如果是大型系统,则要使用Bit State Hsshing的方法选择性搜索一些状态空间；（7）SPIN验证采用多种优化技术,例如状态向量压缩、态压缩、数据流分析、偏序归纳、状态的最小自动机编码以及切片算法等.这些技术大大提高了SPIN的检测速率.

二、SPIN的基本结构

SPIN先从系统模型规格的描述开始,如果检测完不存在语法错误的问题,才进行系统的交互模拟,一直到确定系统设计达到了事先要求的行为.最后,SPIN会生成一个on-the-fly的优化验证程序,并由检测器先进行编译后采用,如果在验证中出现了违反正确性的任何一个反例,就必须退回到交互模拟状态再次进行仔细检测,找到不支持的原因.

把Promela作为系统的规约语言,它只会给有关的进程行为建模并采用SPIN验证,不关心与进程交互没关系的其他元素.Promela语言包括信息通道、进程和变量.其中进程是用来记录系统的行为,而信息通道与变量则是用来描述进程执行时的环境.是以进程作为单位,进程异步组合方式来进行建模,而对于进程的同步则需要额外进行声明.SPIN检测器的基本数据结构主要包括：状态矢量、Seen state set和Depth-first stack.

三、SPIN的工作原理

SPIN工具是用来检测一个有限状态的系统能否达到LTL公式表示的性质的要求,譬如死锁和可达性等.它是用这样一个建模方法：先对进程模板进行定义,给每一个进程模板制定一类进程的行为法则,这样系统可以被当作是一个或者多个进程模板的异步组合.进程所表示的要素一般有条件语句、赋值语句、通讯语句、循环语句和非确定语句.

SPIN建立自动机模型一般使用on-the-fly机制,SPIN检测器能为每一个进程模板提供一个Bochi自动机,然后利用计算自动机异步交错积来获知并发系统的整体行为,具体方法是：（1）最先通过LTL公示描述的系统性质选取反Bochi的自动机A；（2）根据计算机系统的每一个进程所转移子系统数量的乘积,计算出系统的整体行为,用来搭建Bochi自动机P；（3）算出自动机A与P的乘积结果；（4）依次类推得到最后的自动机,验证它是否能接受到语言,如果接受的语言为空,就满足系统定义的属性的要求,反之则不满足.验证具体方法是先检验有没有一个从初始状态开始可达的环路包括至少一个接受状态,用此来验证积自动机接受是不是为空.如果系统不满足条件,那么所产生的自动机组合中肯定有一个可接受回路,而正是这个回路通过动作路径方式体现反例.

SPIN使用深度优先算法来获取每一个积自动机.在经过每一个自动机的途中,SPIN采用偏序简化技术,使状态图更简化,从而达到缓解状态空间不足的问题.此外,SPIN通过具体分析,把每一个局部进程相对应的状态相应地减小.这样把整体状态序号变成一个个局部状态序号的结合,不但能大大减小运行时间外,还能大大降低对外的开销.

四、结语

目前SPIN检测器能更自由开放的使用,而且大规模的用在数据通讯、安全协议验证以及最优规划等各种领域.本文主要从发展、结构、特点和工作原理几个方面简单的阐述了SPIN模型检测器,为日后SPIN的应用奠定了良好的基础.