PROMELA

作品数：43被引量：73H指数：5
导出分析报告
相关作者：李祥吴尽昭黄志球唐郑熠孙守卿更多>>
相关机构：贵州大学南京航空航天大学南昌大学北京交通大学更多>>
相关期刊：《计算机技术与发展》《电脑编程技巧与维护》《计算机与数字工程》《计算机与现代化》更多>>
相关基金：国家自然科学基金国家重点基础研究发展计划国家高技术研究发展计划中央高校基本科研业务费专项资金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机应用x
共 条 记 录，以下是1-6
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于Spin的安全协议形式化验证技术被引量：4
《计算机应用》2014年第A02期85-90,共6页冉俊轶 吴尽昭 
国家自然科学基金资助项目(11371003);广西自然科学基金资助项目(2011GXNSFA018154;2012GXNSFGA060003);广西区主席科技资金资助项目(10169-1);广西教育厅科研资助项目(201012MS274)
针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑(LTL)公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协...
关键词：安全协议 形式化验证 Spin模型检测 Promela语义模型 LTL公式 密钥分配中心协议 
CSMA/CD协议的形式化描述与验证被引量：1
《计算机应用》2013年第A02期235-237,268,共4页张涛 袁键 田宏林 
模型检测是协议验证的技术之一。在CSMA/CD协议的验证过程中对该协议进行了简化,忽略了通道时延、退避算法等细节,运用Promela语言进行建模实现。最后,使用模型检测工具SPIN对协议实现的正确性、状态可达性以及可能存在的不可推进循环...
关键词：PROMELA SPIN 协议验证 载波监听多路访问 冲突检测机制 形式化 
基于Spin检测语义Web服务过程模型
《计算机应用》2010年第12期215-218,共4页周瑾 吴尽昭 杨建书 
国家863计划项目(2007AA01Z143);国家973计划项目(2007CB310803);国家自然科学基金资助项目(6087311860973147);北京交通大学科学基金资助项目(2007RC110)
在Web服务组合的实现中,正确高效验证语义Web服务过程的正确性具有重要意义。为了实现语义Web服务过程模型的自动化检测,针对过程模型中的控制流和数据流,阐述了使用Promela语言规范OWL-S过程模型的一般方法。实例和系统原型表明了该方...
关键词：模型检测 Web服务过程模型 SPIN PROMELA 
UML模型检测方法的研究被引量：6
《计算机应用》2007年第10期2493-2497,2500,共6页张频 罗贵明 
国家973计划项目(24CB719400);国家自然科学基金资助项目(60474026);清华大学基础基金资助
统一建模语言(UML)是设计和分析软件系统最常用的方法,如何保证UML模型满足某些特性是一个非常重要的问题,而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器(SPIN)对UML模型进行检测的方法。首先对...
关键词：模型检测 统一建模语言 层次自动机 简单进程元语言解释器 PROMELA 
Petri网模型的扩展与检测
《计算机应用》2007年第1期183-185,共3页姜洋 罗贵明 
清华大学基础研究基金资助项目(JCPY2005060);清华亚洲基金资助项目(2005B1)
扩展了基本Petri网,提出了更加适合模型检测的MCPN方法,并将MCPN模型转换成模型检测工具SPIN的输入语言———PROMELA。使用SPIN完成对系统模型的检测,以提高软件设计的可靠性。在转换过程中,考虑了对当前情态下处于激活状态的多个变迁...
关键词：PETRI网 模型检测 PROMELA 公平性 
密码协议的Promela语言建模及分析被引量：11
《计算机应用》2005年第7期1548-1550,共3页龙士工 王巧丽 李祥 
贵州省自然科学基金资助项目(20043029)
给出了利用SPIN模型检测分析密码协议的一般方法。作为一个实例,对NeedhamSchroeder公钥密码协议用Promela语言建模,并利用SPIN进行了分析验证,发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析。
关键词：密码协议 模型检测 SPIN PROMELA 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部