摘要：介绍了使用模型验证工具spin检测软件设计阶段存在的安全漏洞的方法.用LTL描述安全属性,将软件设计转换为PROMELA.通过一个关注时序安全属性的实际案例,证明了该方法的可行性.

摘要：在地下建筑智能化系统中,设备监控系统是基本的组成部分,其软件设计的正确性十分重要。提出了一种基于spin的地下建筑设备监控系统软件正确性验证方法。构建了基于iFIX组态软件的设备控制系统软件Promela模型,利用spin模型检验方法对其安全性进行了验证。还利用简化模型进行反例追踪,找出了安全性规约中存在的错误。检验结果表明提出的验证方法是有效性。

摘要：文中详细介绍了无线传感网络面临的安全威胁和密钥管理模型,深入分析了无线传感网体系结构的特点,从密钥管理、身份认证和能耗角度考虑WSN的安全问题,在spin安全协议密钥预分配模型的基础上,引入数字签名身份认证技术,设计符合应用的安全路由算法。

摘要：通信协议的设计与分析是十分困难的工作。使用传统的方法已经难以保证协议设计的效率与质量,针对这一问题,提出了采用spin模型检测技术对通信协议进行分析的方法。以停等式ARQ协议为实例,抽象出它的模型并以Promela语言进行实现。同时,对协议的安全属性进行了分析,并转化为线性时序逻辑公式进行自动验证。最后,分析了停等式ARQ协议的缺陷,并在spin模型检测器中进行了验证。

摘要：快速密钥交换协议JFK是一种新型的密钥交换协议,它的安全性引起了人们的重视.论文对密钥交换协议交换过程进行分析的基础上,使用Promela语言描述了协议模型,并用LTL刻画了需要满足的性质,最后对协议验证结果分析,表明该协议满足其设计目标.

摘要：模型检测是一种有着自动化并能提供反例的验证系统属性的形式化分析方法,其由系统模型,系统属性的描述和模型检测器组成。模型检测器接受模型和属性自动的去验证属性是否满足模型,如果不满足给出一个反例,其在软硬件验证中都得到了广泛的应用。模型检测器spin是由贝尔实验室开发的一种适合于并发系统的模型检测工具。本文在介绍了spin的设计和结构,分析了其理论基础,并通过具体例子阐述了安装和使用模型检测器spin和它的图形化界面ispin的使用方法。spin接受Promela语言建立的模型和使用线性时序逻辑LTL描述的性质,给出验证结果。本文在研究模型检测工具spin的结构和原理的基础上,详细的阐述了其图形化界面ispin的安装和使用。

摘要：遥控玩具纳米零重力遥控车加拿大spin Master公司的Air Hogs系列遥控玩具别具创新特色。刚刚在4月上市的＂纳米零重力遥控车Mini Cooper S＂以真实车型为蓝本设计,尺寸迷你精致。它配备“零重力”系列的神奇攀爬能力，能在墙壁甚至天花板上奔跑。

摘要：为保证关键软件系统的安全性和可靠性,对软件失效模式与影响分析方法在实际应用中存在的问题进行了分析研究,结合模型检验技术提出了一种基于spin的系统级失效模式与影响分析方法。该方法运用spin模型检验工具的验证和模拟功能,有效提高了失效模式分析的准确性和充分性。此外还结合某型航空发动机控制系统介绍了一个应用实例,证明了该方法在工程实践中的可行性。

摘要：由于无线传感器网络(WSN)节点的能量有限,因此尽量减少各节点的能量消耗,延长整个网络的生命周期,是无线传感器网络路由协议设计中考虑的主要问题。文章提出了一种改进的spin路由协议,取名为spin-Z,与现有的spin协议比较,其主要特点是通过减少整个网络冗余数据的传输来减少能量消耗。在NS2环境下进行仿真,结果表明spin-Z协议比spin协议更加节省能量。

摘要：统一建模语言(UML)是用于软件分析与设计的可视化建模语言,由于其缺乏精确的语义描述,因而进一步分析和验证比较困难.而形式化分析方法具有精确的数学语义和自动化验证工具的支持,可以对软件规范进行严格的分析和验证.本文提出了一种将安全协议的可视化模型转换成PROMELA规范的方法,使用spin工具对安全协议UML可视化模型进行了分析验证.