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

作者：林荣峰; 施健; 朱晏庆; 沈怡颹; 周宇

来源：计算机工程, 2019, 45(10): 70-77.

DOI：10.19678/j.issn.1000-3428.0054411

• 航天器系统
• 形式化验证
• 高安全性应用开发环境
• 安全攸关领域
• 模型检查
• 时序性质

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

• 单位
  上海航天控制技术研究所; 华东师范大学