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

摘要：

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

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

所属期刊栏目：45

分类号：TP31(计算技术、计算机技术)

资助基金：国家部委基金

在线出版日期：2019-11-11（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：70-77