基于STP方法的SCADE模型形式化验证框架

• 作者: 周宇 施健 朱晏庆 林荣峰 沈怡颹
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 航天器系统 形式化验证 高安全性应用开发环境 安全攸关领域 模型检查 时序性质
• 年，卷（期）: 2019,（10）
• 所属期刊栏目: 体系结构与软件技术
• 页码范围: 70-77
• 页数: 8页
• 分类号: TP31
• 字数: 6731字
• 语种: 中文
• DOI: 10.19678/j.issn.1000-3428.0054411

摘要

高安全性应用开发环境(SCADE)的形式化验证组件Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质,但不能充分描述拥有复杂时序性质的安全需求.为解决该问题,构建一种SCADE状态机的时序性质验证框架,将SCADE模型转换成NuSMV模型,并将线性时态逻辑和计算树逻辑引入SCADE模型的需求规范中.分析结果表明,借助NuSMV模型检查器及其验证结果可检验复杂时序相关的安全性质,减少模型设计阶段的错误,提高系统的安全性和可靠性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	林荣峰		7	14	2.0	3.0
2	朱晏庆		3	2	1.0	1.0
3	周宇		6	9	2.0	3.0
4	沈怡颹		4	0	0.0	0.0
5	施健	华东师范大学国家可信嵌入式软件工程技术研究中心	1	0	0.0	0.0