计算机工程

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

单位：1. 上海航天控制技术研究所, 上海 201108;2. 华东师范大学 国家可信嵌入式软件工程技术研究中心, 上海 200062

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

基金：国家部委基金。

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

来源：2019年第10期

《计算机工程》期刊编辑部

查看计算机工程杂志2019年第10期