PROMELA

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

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于PROMELA的卫星自主控制逻辑安全性分析方法
《电脑编程技巧与维护》2024年第3期174-176,共3页赵景晖 
随着微处理技术的发展,卫星自主控制逻辑日趋复杂。传统的使用流程图、程序走查、单元测试、系统测试的方法,存在过于依赖相关人员主观能力和无法遍历全部程序执行路径的问题。基于线性时态逻辑的SPIN验证工具可以对使用PROMELA建模的...
关键词：逻辑验证 PROMELA语言 卫星设计 
面向SysML模型的安全性分析与验证方法被引量：4
《计算机科学》2019年第11期100-108,共9页李宛倩 胡军 陈松 张维珺 
国家重点基础研究发展计划-973计划(2014CB744903);国家航空科学基金(20165515001);南京航空航天大学研究生创新基地开放基金(kfjj20171611);中央高校基本科研业务费专项资金资助
近年来,随着航空、交通、医疗等安全关键系统的规模越来越大,涉及到的复杂度也越来越高,基于模型的系统安全性分析与验证成为安全关键系统工程领域的一个重要研究方向,因而如何对以SysML为典型的系统模型进行安全性分析与验证是一个非...
关键词：安全关键系统 SYSML AltaRica3.0 PROMELA 机轮刹车系统 
停等式ARQ协议的SPIN模型检测被引量：1
《福建工程学院学报》2018年第3期253-258,共6页黄丽丽 
介绍停等式ARQ协议的工作原理,并使用Promela对其进行建模,利用SPIN对所建模型进行检测,证明了所建模型具有停等式ARQ协议的性质。讨论对停等式ARQ协议进行攻击的方法,使用Promela语言对攻击者进行建模,并利用SPIN的图形界面工具XSPIN...
关键词：停等式ARQ SPIN PROMELA 模型检测 
AltaRica 3.0模型到Promela模型转换与验证方法研究被引量：6
《计算机工程与科学》2017年第4期708-716,共9页胡军 陈松 王明明 
国家973计划(2014CB744903);回国留学人员科研启动基金;南京航空航天大学青年科技创新基金(NS2014098)
AltaRica语言用于安全关键系统的建模,其拥有一套完整的建模分析工具,但随着AltaRica3.0的更新,ARC等传统的AltaRica建模分析工具已不再支持,而SPIN作为一个穷尽式模型验证工具被广泛应用。介绍了AltaRica3.0相对于之前版本在表达能力...
关键词：安全关键系统 AltaRica3.0 SPIN 机轮刹车系统 
RGPS服务层元模型正确性验证
《软件导刊》2016年第12期8-10,共3页张莉 杨淑贞 杨浩 
浙江省教育厅一般科研项目(2016);浙江省教育中心2014年研究课题(JA049)
随着网络式软件复杂程度的日益增加,如何确保网络式软件功能和性能的正确性越发重要。根据网络式软件的特点,在RGPS需求元建模框架的指导下,提出RGPS服务层元模型正确性验证。首先用BPEL语言和WSDL语言把RGPS服务层元模型描述成BPEL模型...
关键词：网络式软件 BPEL PROMELA LTL公式 正确性验证 
基于SPIN的功能测试用例生成方法研究
《软件导刊》2016年第7期1-4,共4页李建 杨晋吉 
国家自然科学基金项目(61272066)
提出了一种自动生成系统功能测试用例的新方法。该方法使用Promela语言对软件系统的状态和行为进行描述建模,使用LTL公式描述测试覆盖标准,然后将该组LTL公式和描述状态行为的Promela模型输入SPIN模型检测工具,并利用模型检测工具自动...
关键词：功能测试用例 SPIN 模型检测 Promela建模 
通信协议的Promela语言建模与检测被引量：1
《福建电脑》2016年第3期39-40,50,共3页陈义 唐郑熠 
福建省中青年教师教育科研项目(JA15336;JB14069);福建工程学院科研发展基金资助项目(GY-Z15087)
通信协议的设计与分析是十分困难的工作。使用传统的方法已经难以保证协议设计的效率与质量,针对这一问题,提出了采用SPIN模型检测技术对通信协议进行分析的方法。以停等式ARQ协议为实例,抽象出它的模型并以Promela语言进行实现。同时,...
关键词：通信协议 ARQ协议 模型检测 SPIN PROMELA 
基于Spin的地铁门控制系统建模与验证被引量：1
《西安邮电大学学报》2015年第5期57-61,共5页舒新峰 张炎龙 孙林泽 
国家自然科学基金资助项目(61050003);陕西省教育厅自然科学基金资助项目(11JK1037)
针对地铁门控制系统(MDCS)安全问题,提出一种MDCS检测方法。通过分析MDCS的控制逻辑,使用Promela建立了基于Spin的MDCS系统模型,将MDCS中的地铁控制系统、地铁门控制系统及屏蔽门控制系统抽象为三个进程,并用线性时态逻辑公式描述待验...
关键词：地铁门控制系统 模型检测 SPIN PROMELA 
一种基于故障扩展SysML活动图的安全性验证框架研究被引量：4
《计算机科学》2015年第7期222-228,共7页仵志鹏 黄志球 王珊珊 曹德建 
国家自然科学基金(61100034;61170043);中国博士后科学基金(20110491411);江苏省普通高校研究生科研创新计划资助项目;中央高校基本科研业务费专项资金(CXZZ11_0218)资助
随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和Sy...
关键词：安全性验证 故障树语义 SysML活动图 PROMELA 
基于Spin的安全协议形式化验证技术被引量：4
《计算机应用》2014年第A02期85-90,共6页冉俊轶 吴尽昭 
国家自然科学基金资助项目(11371003);广西自然科学基金资助项目(2011GXNSFA018154;2012GXNSFGA060003);广西区主席科技资金资助项目(10169-1);广西教育厅科研资助项目(201012MS274)
针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑(LTL)公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协...
关键词：安全协议 形式化验证 Spin模型检测 Promela语义模型 LTL公式 密钥分配中心协议 
全选清除导出
共5页<12345>
检索报告 对象比较 聚类工具 使用帮助 返回顶部