论文摘要
高安全性应用开发环境(SCADE)的形式化验证组件Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质,但不能充分描述拥有复杂时序性质的安全需求。为解决该问题,构建一种SCADE状态机的时序性质验证框架,将SCADE模型转换成NuSMV模型,并将线性时态逻辑和计算树逻辑引入SCADE模型的需求规范中。分析结果表明,借助NuSMV模型检查器及其验证结果可检验复杂时序相关的安全性质,减少模型设计阶段的错误,提高系统的安全性和可靠性。
论文目录
文章来源
类型: 期刊论文
作者: 林荣峰,施健,朱晏庆,沈怡颹,周宇
关键词: 航天器系统,形式化验证,高安全性应用开发环境,安全攸关领域,模型检查,时序性质
来源: 计算机工程 2019年10期
年度: 2019
分类: 信息科技,工程科技Ⅱ辑
专业: 航空航天科学与工程
单位: 上海航天控制技术研究所,华东师范大学国家可信嵌入式软件工程技术研究中心
基金: 国家部委基金
分类号: V446
DOI: 10.19678/j.issn.1000-3428.0054411
页码: 70-77
总页数: 8
文件大小: 421K
下载量: 117
相关论文文献
- [1].The MathWorks为安全关键系统提供自动化模型检查支持[J]. 电信科学 2008(05)
- [2].有界模型检查可执行文件的安全属性[J]. 小型微型计算机系统 2008(09)
- [3].基于模型检查的货运飞船推进剂在轨补加任务故障树分析方法研究[J]. 质量与可靠性 2018(06)
- [4].面向模型检查的NuSMV统一建模方法[J]. 系统工程与电子技术 2018(07)
- [5].一种基于模型检查的嵌入式软件验证方法[J]. 单片机与嵌入式系统应用 2009(05)
- [6].程序模型检查器综述[J]. 计算机科学 2009(04)
- [7].基于限界模型检查的Web服务行为失配检测[J]. 计算机科学 2012(06)
- [8].时态认知逻辑CTL*K的符号化模型检查算法[J]. 计算机科学 2009(05)
- [9].基于规则设定的全方位碰撞检查技术[J]. 建筑与文化 2014(08)
- [10].面向对象的CAD模型检查方法研究[J]. 制造业自动化 2009(04)
- [11].异构多智能体系统模型检查[J]. 软件学报 2018(06)
- [12].基于CATIA二次开发技术的模型质量检查[J]. 新技术新工艺 2015(01)
- [13].SOC的形式化验证方法[J]. 武汉大学学报(工学版) 2008(06)
- [14].BIM模型智能检查工具研究与应用[J]. 土木建筑工程信息技术 2018(02)
- [15].PROMELA语义引擎执行研究[J]. 电脑知识与技术 2008(35)
- [16].RPKI增量同步Delta协议的形式化检测与实现[J]. 计算机系统应用 2018(11)
- [17].基于模型检查的嵌入式软件构件化分析与验证[J]. 现代电子技术 2016(24)
- [18].模型检查在测试用例生成中的应用[J]. 常熟理工学院学报 2008(10)
- [19].SMV的观察迁移系统的模型检测分析[J]. 计算机工程与设计 2008(18)
- [20].区间时序逻辑的模型检查[J]. 西安电子科技大学学报 2009(02)
- [21].SPIN语义引擎执行方式研究[J]. 计算机与现代化 2009(11)
- [22].基于并行环境的模型检查技术研究与实现[J]. 太原师范学院学报(自然科学版) 2012(02)
- [23].程序切片技术在并发程序模型检查中的应用[J]. 计算机技术与发展 2008(11)
- [24].一种新的Statechart模型验证方法[J]. 计算机科学 2011(02)
- [25].BIM系列软件在建筑碰撞检查时的应用[J]. 山东工业技术 2019(03)
- [26].一种基于System C语言的模型检测方法[J]. 广西民族大学学报(自然科学版) 2016(03)
- [27].XML Schema特征提取算法[J]. 计算机科学 2015(S2)
- [28].多速率混合系统的模型检查[J]. 西安电子科技大学学报 2008(01)
- [29].业务过程模型的Petri网形式化检查方法[J]. 计算机集成制造系统 2011(05)
- [30].Pro/E二次开发在模型检查技术中的应用[J]. 计算机仿真 2013(08)
标签：航天器系统论文; 形式化验证论文; 高安全性应用开发环境论文; 安全攸关领域论文; 模型检查论文; 时序性质论文;