期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到64篇文章
< 1 2 … 4 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
IKEv2协议的SPIN模型检测 被引量：9
1
作者 陈大伟 董荣胜 +1 位作者 郭云川 古天龙 《计算机工程》 CAS CSCD 北大核心 2006年第5期164-166,246,共4页
基于模型检测技术,使用SPIN对IKEv2协议进行了建模和分析。应用Promela语言描述了协议模型,并用LTL规约了该协议需要满足的认证性和秘密性,最后对检测结果进行了分析。
关键词 IKE协议 模型检测 SPIN promela
下载PDF
密码协议的Promela语言建模及分析 被引量：11
2
作者 龙士工 王巧丽 李祥 《计算机应用》 CSCD 北大核心 2005年第7期1548-1550,共3页
给出了利用SPIN模型检测分析密码协议的一般方法。作为一个实例,对NeedhamSchroeder公钥密码协议用Promela语言建模,并利用SPIN进行了分析验证,发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析。
关键词 密码协议 模型检测 SPIN promela
下载PDF
UML模型检测方法的研究 被引量：6
3
作者 张频 罗贵明 《计算机应用》 CSCD 北大核心 2007年第10期2493-2497,2500,共6页
统一建模语言(UML)是设计和分析软件系统最常用的方法,如何保证UML模型满足某些特性是一个非常重要的问题,而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器(SPIN)对UML模型进行检测的方法。首先对... 统一建模语言(UML)是设计和分析软件系统最常用的方法,如何保证UML模型满足某些特性是一个非常重要的问题,而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器(SPIN)对UML模型进行检测的方法。首先对UML模型进行形式化描述,使用层次自动机来描述状态图,然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA,使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束,通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。 展开更多
关键词 模型检测 统一建模语言 层次自动机 简单进程元语言解释器 promela
下载PDF
基于SPIN的IKEv2协议高效模型检测 被引量：5
4
作者 吴昌 肖美华 《计算机工程与应用》 CSCD 北大核心 2008年第5期158-161,共4页
论文先简单介绍了互联网密钥交换协议IKEv2,然后利用著名的模型检测工具SPIN对其进行了建模和分析。在建模的过程中,作者发现现有的建模方法很难对结构复杂的协议IKEv2进行建模,而且用现有的建模方法建立的模型可读性差、自动化程度不高... 论文先简单介绍了互联网密钥交换协议IKEv2,然后利用著名的模型检测工具SPIN对其进行了建模和分析。在建模的过程中,作者发现现有的建模方法很难对结构复杂的协议IKEv2进行建模,而且用现有的建模方法建立的模型可读性差、自动化程度不高,验证效率也比较低,因此现有的建模方法只适用于对简单协议进行建模。针对这些不足之处,提出了一种程序可读性、自动化程度及验证效率均较好的建模方法,而且这种建模方法特别适合对复杂的安全协议进行建模。最后利用SPIN对IKEv2协议的模型进行了验证,发现IKEv2协议不能抵御主动攻击,并给出了两个攻击序列图。针对IKEv2协议不能保护发起者身份的缺陷,提出了自己的一种改进意见。 展开更多
关键词 IKEV2 模型检测 SPIN promela IP隧道
下载PDF
基于Spin的SysML活动图验证框架 被引量：6
5
作者 胡良文 马金晶 孙博 《计算机科学与探索》 CSCD 2014年第7期836-847,共12页
系统建模语言(systems modeling language,SysML)缺乏精确的形式化分析和验证手段,造成模型存在死锁、活锁等诸多问题,可以通过形式化验证方法来提高模型的正确性。然而,受制于传统的形式化方法需要复杂的公式推理,并且不易理解等方面... 系统建模语言(systems modeling language,SysML)缺乏精确的形式化分析和验证手段,造成模型存在死锁、活锁等诸多问题,可以通过形式化验证方法来提高模型的正确性。然而,受制于传统的形式化方法需要复杂的公式推理,并且不易理解等方面局限性,大多数验证仅限专家使用并且很耗时。为了克服SysML模型中存在的问题,提出了一种针对SysML多层次活动图的分析验证框架。它可以根据已构建的模型,将多层次活动图分解转换为Spin的输入模型,并对相关子图进行重组和验证。实验表明,该方法可以有效识别多层次活动图,并准确实施转换,为模型验证的演化提供支持。 展开更多
关键词 系统建模语言(SysML) 活动图 模型验证 SPIN promela
下载PDF
TCP协议的安全性和活性验证 被引量：3
6
作者 陈道喜 陈冬火 张广泉 《苏州大学学报（自然科学版）》 CAS 2008年第1期54-59,64,共7页
网络协议簇中,传输控制协议TCP是最重要的协议之一,提供面向连接的可靠传输服务.采用Promela描述TCP建立连接和可靠数据传输,并用模型检测工具Spin,验证TCP三次握手协议的安全性与可靠数据传输协议活性的属性.
关键词 TCP promela SPIN 模型检测
下载PDF
一种基于故障扩展SysML活动图的安全性验证框架研究 被引量：4
7
作者 仵志鹏 黄志球 +1 位作者 王珊珊 曹德建 《计算机科学》 CSCD 北大核心 2015年第7期222-228,共7页
随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和Sy... 随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和SysML活动图两种模型语义描述的基础上,提出了一种基于故障扩展SysML活动图的安全性验证框架,包括:首先利用故障树最小割集提取故障信息并给出故障树逻辑门的转换规则;然后给出故障扩展SysML活动图的构建步骤;最后使用Promela对故障扩展SysML活动图进行建模,并使用模型检测工具SPIN对其进行分析验证。通过一个燃气灶控制系统验证了此方法的有效性。 展开更多
关键词 安全性验证 故障树语义 SysML活动图 promela
下载PDF
基于SPIN的无线传感器网络安全协议建模与分析 被引量：4
8
作者 敬超 常亮 古天龙 《计算机科学》 CSCD 北大核心 2009年第10期132-136,共5页
模型检验方法在有线网安全协议的分析和设计方面取得了巨大成功。无线传感器网络对安全协议同样具有严格的要求;与有线网相比,无线传感器网络在通信环境和网络节点等方面都更为脆弱,为相应的安全协议的分析和设计提出了挑战。提出了一... 模型检验方法在有线网安全协议的分析和设计方面取得了巨大成功。无线传感器网络对安全协议同样具有严格的要求;与有线网相比,无线传感器网络在通信环境和网络节点等方面都更为脆弱,为相应的安全协议的分析和设计提出了挑战。提出了一种适用于无线传感器网络的安全协议形式化建模分析方法。它充分借鉴了传统有线网络安全协议的建模方法,在其基础上充分考察了无线传感器网络的通信环境以及网络节点,建立起一个全面并且直观的安全协议运行模型。以A.Perrig等人提出的SPINS安全协议为例,应用模型检验工具SPIN对其认证性和机密性等安全需求进行了分析验证,发现了该协议存在的漏洞。实例分析证实了模型检验方法在分析无线传感器网络安全协议时的有效性,从而推进了其在安全协议分析方面的应用范围。 展开更多
关键词 无线传感器网络 模型检验 SPINS协议 SPIN工具 promela
下载PDF
面向SysML模型的安全性分析与验证方法 被引量：4
9
作者 李宛倩 胡军 +1 位作者 陈松 张维珺 《计算机科学》 CSCD 北大核心 2019年第11期100-108,共9页
近年来,随着航空、交通、医疗等安全关键系统的规模越来越大,涉及到的复杂度也越来越高,基于模型的系统安全性分析与验证成为安全关键系统工程领域的一个重要研究方向,因而如何对以SysML为典型的系统模型进行安全性分析与验证是一个非... 近年来,随着航空、交通、医疗等安全关键系统的规模越来越大,涉及到的复杂度也越来越高,基于模型的系统安全性分析与验证成为安全关键系统工程领域的一个重要研究方向,因而如何对以SysML为典型的系统模型进行安全性分析与验证是一个非常重要的问题。文中以基于模型的安全性分析(MBSA)为框架,设计了一个面向SysML模型的系统安全性分析与验证方法,实现了从模型构建到安全性分析与属性验证的完整过程。首先,从需求层面和设计层面对SysML系统架构设计模型和最新系统安全性建模语言AltaRica3.0进行了介绍,构建了从SysML的核心模型元素到AltaRica3.0模型的语义等价的转换规则,给出了转换规则的形式化描述并分析证明转换规则的正确性;然后,基于模型驱动的方法设计了一个原型工具平台来完成模型的自动转换和安全性分析过程,该原型工具集成了转换、编译生成故障树、故障树分析、单步仿真及故障路径动态演示等功能,实现了系统设计和安全性分析的同步性,并在此基础上给出了AltaRica3.0至Promela模型的转换关键点,结合穷尽式模型验证工具SPIN对模型的属性进行安全性验证;最后,根据4761标准中对机轮刹车系统的体系结构设计描述和安全性的需求建立SysML模型,依据原型工具平台和属性验证工具实现模型的自动转换和安全性分析验证,进而来说明此转换方法的有效性。 展开更多
关键词 安全关键系统 SYSML AltaRica3.0 promela 机轮刹车系统
下载PDF
一种自动化模型检测ANSI-C程序的实用方法 被引量：4
10
作者 王大伟 张大方 缪力 《计算机工程与科学》 CSCD 北大核心 2010年第4期79-82,共4页
模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法。为了利用模型检测技术,通常的办法是手工构建一个抽象模型,然而这个方法存在一些不足,如成本过高、易引入建模错误等。本文提出了一种自动化模型检测ANSI-C程序的方法,并开... 模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法。为了利用模型检测技术,通常的办法是手工构建一个抽象模型,然而这个方法存在一些不足,如成本过高、易引入建模错误等。本文提出了一种自动化模型检测ANSI-C程序的方法,并开发了模型提取工具C2Spin,它能够分析ANSI-C源代码,并生成对应的PROMELA验证模型,从而显著降低了建模的开销。利用C2Spin,模型检测工具SPIN可以自动地检测使用C语言编写的应用程序中的多种错误,如死锁等。在初步实验中,依靠C2Spin生成的模型,我们发现了SPIN4.3.0的一个语义错误,以及Holzmann对两个经典互斥算法的实现程序中的活锁错误。这些结果表明,C2Spin能够帮助人们更加快速有效地测试C程序。 展开更多
关键词 形式化方法 模型检测 模型提取 ANSI-C promela
下载PDF
针对A(0)协议的新鲜性攻击及改进方案 被引量：2
11
作者 唐郑熠 李均涛 李祥 《计算机技术与发展》 2009年第10期164-166,共3页
非形式化方法很难保证认证协议的安全性,因此对于形式化方法的研究与应用具有重要的意义,模型检测技术就是其中的一种。该文介绍了使用模型检测工具SPIN和Promela语言对A(0)协议进行建模检测的方法,并从检测结果中发现了A(0)协议无法保... 非形式化方法很难保证认证协议的安全性,因此对于形式化方法的研究与应用具有重要的意义,模型检测技术就是其中的一种。该文介绍了使用模型检测工具SPIN和Promela语言对A(0)协议进行建模检测的方法,并从检测结果中发现了A(0)协议无法保证公开协商密钥证书新鲜性的缺陷。据此设计出了针对A(0)协议的新鲜性攻击方法,并提出了弥补其新鲜性缺陷的改进方案。由此可见,使用模型检测技术可以高效便捷地对认证协议进行分析。 展开更多
关键词 A(0) 新鲜性 协议攻击 模型检测 SPIN promela
下载PDF
基于Promela的UML建模方法及其应用 被引量：2
12
作者 舒良春 饶俊 +1 位作者 肖美华 尹传文 《计算机与现代化》 2010年第2期101-104,共4页
针对形式化方法与可视化方法的优缺点,本文提出形式化方法与可视化UML互补的建模方法,主要探讨用形式化方法验证UML模型,将UML模型转换为Promela模型,再用模型检测工具SPIN对Promela模型进行验证。最后通过实例对此转换方法进行验证,实... 针对形式化方法与可视化方法的优缺点,本文提出形式化方法与可视化UML互补的建模方法,主要探讨用形式化方法验证UML模型,将UML模型转换为Promela模型,再用模型检测工具SPIN对Promela模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。 展开更多
关键词 UML promela SPIN 形式化方法
下载PDF
CSMA/CD协议的形式化描述与验证 被引量：1
13
作者 张涛 袁键 田宏林 《计算机应用》 CSCD 北大核心 2013年第A02期235-237,268,共4页
模型检测是协议验证的技术之一。在CSMA/CD协议的验证过程中对该协议进行了简化,忽略了通道时延、退避算法等细节,运用Promela语言进行建模实现。最后,使用模型检测工具SPIN对协议实现的正确性、状态可达性以及可能存在的不可推进循环... 模型检测是协议验证的技术之一。在CSMA/CD协议的验证过程中对该协议进行了简化,忽略了通道时延、退避算法等细节,运用Promela语言进行建模实现。最后,使用模型检测工具SPIN对协议实现的正确性、状态可达性以及可能存在的不可推进循环进行了分析和检验,并从结果的有效性和正确性方面得出了相应验证输出图。 展开更多
关键词 promela SPIN 协议验证 载波监听多路访问 冲突检测机制 形式化
下载PDF
基于Spin的地铁门控制系统建模与验证 被引量：1
14
作者 舒新峰 张炎龙 孙林泽 《西安邮电大学学报》 2015年第5期57-61,共5页
针对地铁门控制系统(MDCS)安全问题,提出一种MDCS检测方法。通过分析MDCS的控制逻辑,使用Promela建立了基于Spin的MDCS系统模型,将MDCS中的地铁控制系统、地铁门控制系统及屏蔽门控制系统抽象为三个进程,并用线性时态逻辑公式描述待验... 针对地铁门控制系统(MDCS)安全问题,提出一种MDCS检测方法。通过分析MDCS的控制逻辑,使用Promela建立了基于Spin的MDCS系统模型,将MDCS中的地铁控制系统、地铁门控制系统及屏蔽门控制系统抽象为三个进程,并用线性时态逻辑公式描述待验证性质,运行Spin后即可判断MDCS是否存在安全隐患。实验结果表明,该检测方法可有效验证MDCS的安全性。 展开更多
关键词 地铁门控制系统 模型检测 SPIN promela
下载PDF
SPIN语义引擎执行方式研究 被引量：1
15
作者 黎升洪 冯艳清 《计算机与现代化》 2009年第11期112-115,共4页
模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。本文从语义角度研究PROMELA语义引擎问题,首先给出PROMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PROMELA语法到抽象对... 模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。本文从语义角度研究PROMELA语义引擎问题,首先给出PROMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PROMELA语法到抽象对象模型的映射,描述PROMELA指称语义。最后针对SPIN中atomic序列和同步通信等复杂问题给出解决方法。 展开更多
关键词 模型检查 SPIN promela 语义
下载PDF
基于SPIN的系统建模研究 被引量：1
16
作者 徐小丽 《计算机与现代化》 2012年第9期209-214,共6页
模型检测由于其自动化程度高,是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器,首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理,并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行... 模型检测由于其自动化程度高,是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器,首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理,并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行模型,并对实验结果进行分析。 展开更多
关键词 模型检测 建模 SPIN promela
下载PDF
停等式ARQ协议的SPIN模型检测 被引量：1
17
作者 黄丽丽 《福建工程学院学报》 CAS 2018年第3期253-258,共6页
介绍停等式ARQ协议的工作原理,并使用Promela对其进行建模,利用SPIN对所建模型进行检测,证明了所建模型具有停等式ARQ协议的性质。讨论对停等式ARQ协议进行攻击的方法,使用Promela语言对攻击者进行建模,并利用SPIN的图形界面工具XSPIN... 介绍停等式ARQ协议的工作原理,并使用Promela对其进行建模,利用SPIN对所建模型进行检测,证明了所建模型具有停等式ARQ协议的性质。讨论对停等式ARQ协议进行攻击的方法,使用Promela语言对攻击者进行建模,并利用SPIN的图形界面工具XSPIN模拟了攻击过程,验证了攻击的有效性。 展开更多
关键词 停等式ARQ SPIN promela 模型检测
下载PDF
基于SPIN的SSL3.0握手协议模型检测 被引量：1
18
作者 程莹 康汶 《计算机与数字工程》 2010年第8期156-159,共4页
文章介绍了密钥交换协议SSL3.0协议,并利用模型检测工具SPIN对其进行了形式化分析、建模和验证。实验结果表明此验证方法的正确性,证明了协议本身的安全性与可行性,并且提高了协议的验证效率。
关键词 SSL3.0 模型检测 SPIN promela LTL
下载PDF
Petri网性质的线性时序逻辑描述与Spin检验 被引量：1
19
作者 段风琴 李祥 《计算机科学》 CSCD 北大核心 2006年第5期287-289,共3页
Petri 网是描述并发系统的很直观的图形工具;Spin 是一种著名的分析验证并发系统性质的工具。本文首先论述 Petri 网性质的线性时序逻辑描述,研究用 Promela 编程描述 Petri 网和用 Spin 对 Petri 网性质进行检验的方法,最后通过两个具... Petri 网是描述并发系统的很直观的图形工具;Spin 是一种著名的分析验证并发系统性质的工具。本文首先论述 Petri 网性质的线性时序逻辑描述,研究用 Promela 编程描述 Petri 网和用 Spin 对 Petri 网性质进行检验的方法,最后通过两个具体的示例说明这种方法是成功的。 展开更多
关键词 模型检测 SPIN promela PETRI网 线性时序逻辑
下载PDF
基于连续ARQ协议的隐蔽洪水攻击
20
作者 赵梦龙 唐郑熠 《计算机技术与发展》 2012年第10期177-180,共4页
通信协议设计时的疏漏很容易造成严重的后果,因此有必要采用形式化的方法来保证协议的安全性和可靠性。模型检测是一种具有工业应用前景的形式化分析方法,并具有很高的自动化程度,适合于协议的分析与验证。文中采用模型检测工具SPIN对连... 通信协议设计时的疏漏很容易造成严重的后果,因此有必要采用形式化的方法来保证协议的安全性和可靠性。模型检测是一种具有工业应用前景的形式化分析方法,并具有很高的自动化程度,适合于协议的分析与验证。文中采用模型检测工具SPIN对连续ARQ协议建模,通过验证该协议的基本属性证明所建模型的正确性。然后依据Dolev和Yao的思想加入攻击者模型再进行分析,发现了连续ARQ协议的一个新漏洞,攻击者能够利用这个漏洞造成大量冗余数据的传输和存储。这种攻击建立在互信的数据传输基础上,且攻击者并不直接发送冗余数据,因此具有很高的隐蔽性。 展开更多
关键词 连续ARQ协议 洪水攻击 模型检测 SPIN promela
下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 2 … 4 下一页 到第 页
使用帮助 返回顶部