基于SPIN／Promela的并发系统验证

并发系统安全性分析是当前计算机科学中一个重要的研究领域。模型检测是最成功的自动验证技术之一，其成功应用归功于有效验证工具的支持。SPIN是一种著名的分析验证并发系统逻辑一致性的工具。本文在阐述SPIN工作机理的基础上，详细分析了基于SPIN的系统建模语言Promela中通道操作、基本数据结构及其功能，并设计了SPIN形式化验证软件系统的基本算法，最后运用SPIN对一个并发系统实例进行验证，得出了相应验证输出图。     

WTP协议的SPIN模型检测

基于模型检测技术,使用SPIN对WTP协议进行了建模和分析．应用自动机和Promela对协议进行建模。利用LTL规范了协议需要满足的安全性,时序性。通过分析发现了协议的一个错误。     

WTP协议的SPIN模型检测

基于模型检测技术,使用SPIN对WTP协议进行了建模和分析.应用自动机和Promela对协议进行建模,利用LTL规范了协议需要满足的安全性,时序性。通过分析发现了协议的一个错误。     

基于SPIN内核的SDL模型检验工具设计

规格描述语言SDL目前广泛应用于复杂通信协议和软件系统的建模。使用模型检验技术对SDL进行分析和验证可以检测出模型中的逻辑错误,大大提高SDL建模结果的精确性。论文研究了SDL的形式化语义SDL/PR中常用部分与模型检验工具SPIN的输入语言Promela之间的语义映射规则,并以此为基础开发了一个基于SPIN内核的SDL模型检验器SSMC Tool。     

IKEv2协议的SPIN模型检测

基于模型检测技术,使用SPIN对IKEv2协议进行了建模和分析。应用Promela语言描述了协议模型,并用LTL规约了该协议需要满足的认证性和秘密性,最后对检测结果进行了分析。     

基于SPIN的HMSC模型自动检验方法

自动检测与验证HMSC (high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义，为此提出一种为HMSC模型进行自动检验的方法，并将其实现。利用转换规则为HMSC模型生成Promela检测语言，借助SPIN工具对需求进行验证。该方法不仅支持模型检测，同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具，通过一个实例展示其自动建模检测分析的效果，表明了其有效性和实用性。     

基于SPIN的G语言系统模型的验证

对于大型系统,为确保其运行的可靠性、稳定性及高效性,需要从两个方面对系统进行验证:业务模型和系统模型。目前,对业务模型的验证可通过BPMN来完成;对系统模型的验证可通过SPIN(Simple Promela Interpreter)工具执行。G语言是由NI公司创建的一种图形化程序框图语言,还未被加入ANSI标准,因此,文中第一步工作是提取G语言的形式、规则、文法等语言特性。由于SPIN对G语言不提供直接的支持,因此第二步工作是完成G2Promela的映射。在G2Promela的工作中,主要是基于编译器的框架,以Scanner-Parser-Optimizer-Generator(SPOG框架)为主线,根据第一步的预处理工作,按方法函数、指针、关键字、变量等分类创建G2Promela的映射规则,最终实现G2Promela的转换,完成对G语言系统模型的验证。该方法的提出弥补了G语言系统模型验证方面的空白,从而更深入地确保了G语言程序的性能。     

炼焦过程控制计算机故障的分析与模型检测

用模型检测技术分析了工业生产中计算机通讯的一个死锁故障。根据技术人员的分析,建立了该通讯过程的Promela语言模型,并使用SPIN进行检测,找出了发生死锁的原因,其检测结果与技术人员的分析一致。     

UML顺序图与状态图的一致性检查

用户可使用UML从不同角度对系统进行建模,但不同视图间存在信息冗余,可能导致视图不一致问题。该文针对具有多种逻辑语义的顺序图提出分析方法,为复杂层次结构的状态图引入有限状态自动机,利用自动机分解算法得到自动机树。制定新的顺序图和状态图一致性检查准则和Promela代码结构,用模型检验工具SPIN进行顺序图及其相关状态图的一致性检验。     

基于SPIN的地下建筑设备监控系统软件验证

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

密码协议的Promela语言建模及分析

给出了利用SPIN模型检测分析密码协议的一般方法。作为一个实例,对Needham Schroeder 公钥密码协议用Promela语言建模,并利用SPIN进行了分析验证,发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析     

自动生成GEF图形编辑器的研究与实现

针对当前GEF编辑器开发难度大、开发周期长的问题,设计了一个能够自动生成GEF图形编辑器的MDA工具GEG的体系结构。它利用EMF的代码自动生成方法JET和JMerge,以及EMF.edit提供的适配器机制,生成了一个完整的基于Eclipse平台的图形编辑器插件。在系统设计和实现过程中,引入了配置元模型和视图元模型。     

安全协议Andrew RPC的SPIN模型检测

本文运用模型检测技术,以Dolev-Yao模型为基础,提出了使用Promela语言和模型检测工具SPIN对Andrew RPC协议进行建模和分析的方法,发现了该协议存在重放攻击漏洞,该方法具有一定通用性和很好的参考价值。     

面向AltaRica模型的嵌入式系统安全性验证方法

嵌入式系统在航空、航天、交通等安全关键领域的使用愈加广泛,Alta Rica是一种描述安全关键系统的建模语言,同时基于Alta Rica模型的安全性分析已成为欧洲的工业标准。提出了一种面向Alta Rica模型的嵌入式系统安全性验证方法,包括:使用Alta Rica语言对嵌入式系统进行建模;给出Alta Rica模型到Promela模型的转换规则;对转换规则进行形式化证明,得到嵌入式系统的Promela模型;使用模型检验工具SPIN进行安全性验证。通过机轮刹车系统中的机轮刹车控制单元进行实例分析,验证了转换规则的正确性和有效性。     

基于SPIN的系统建模研究

模型检测由于其自动化程度高,是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器,首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理,并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行模型,并对实验结果进行分析。     

AltaRica 3.0模型到Promela模型转换与验证方法研究

AltaRica语言用于安全关键系统的建模,其拥有一套完整的建模分析工具,但随着AltaRica3.0的更新,ARC等传统的AltaRica建模分析工具已不再支持,而SPIN作为一个穷尽式模型验证工具被广泛应用。介绍了AltaRica3.0相对于之前版本在表达能力方面的改进,以及其底层模型GTS的基本结构。以AltaRica3.0扁平化为GTS模型的思想为基础,提出了一种AltaRica3.0模型向Promela模型的转换规则。以民用飞机中机轮刹车系统WBS为例,建立了AltaRica3.0模型,并且通过转换规则转为Promela模型。最后根据民用航空标准SAE ARP 4761中对机轮刹车系统的安全性要求,利用SPIN工具对机轮刹车系统的安全属性进行了验证。     

IEEE802.11中WEP认证协议的SPIN模型检测

用SPIN工具对WEP认证协议进行模型检测,不仅可以从状态空间上搜索出协议的漏洞,还可以各个角度分析WEP协议的运行逻辑.模型检测的方法先通过建立WEP认证协议的模型,转换成SPIN的输入语言Promela,然后通过建立WEP协议的性质转化成LTL语言,最后利用SPIN工具分析WEP认证协议.实验的结果说明WEP认证协议存在漏洞.     

一种模型转换的编织框架

模型转换是MDA(model driven architecture)的核心技术之一,也是目前MDA研究的热点.目前,MDA范畴内存在多种模型转换方法和工具,它们之间的异构性造成了模型转换代码重用的困难,并使学习和使用模型转换方法的成本增加.受到模型编织技术的启发,提出了一种基于QVT(model query/view/transformation)规范的模型转换编织框架QMTW(QVT-based model transformation weaving framework)来解决以上缺点.展示了模型转换编织的概念、语义、元模型和语法,以及到目标语言的转换定义,并以一个具体实例说明了本框架的使用方法和优点.QMTW提高了模型转换的抽象层次,统一了多种模型转换语言,并支持OMG最新的模型转换规范,在一定程度上消除了模型转换技术的异构性,同时具有简单、规范、扩展性强3个优点.     

基于Promela的UML建模方法及其应用

针对形式化方法与可视化方法的优缺点,本文提出形式化方法与可视化UML互补的建模方法,主要探讨用形式化方法验证UML模型,将UML模型转换为Promela模型,再用模型检测工具SPIN对Promela模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。     

TEFL:一种文本式特征建模语言

特征模型已经成为软件产品线工程中共性/可变性建模的事实标准.现有基于特征图的建模工具由于在模型表达能力、严谨的形式化语义等方面的不足限制了其在工业界的应用.为了消除这些建模中的缺陷,为基于特征的产品线开发提供一个坚实的支撑环境,提出文本式特征建模语言TEFL,介绍其具体语法、抽象语法,以及形式化语义;开发一个基于Eclipse的语言编辑器原型;给出了面向XML和Java语言应用转化方法和工具;分析了与现有文本式建模技术相比所具有的优势与不足,并指出在特征建模及其工具技术方面的进一步的工作方向.