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

作     者：林荣峰 施健 朱晏庆 沈怡颹 周宇 LIN Rongfeng;SHI Jian;ZHU Yanqing;SHEN Yiwei;ZHOU Yu

作者机构：上海航天控制技术研究所上海201108 华东师范大学国家可信嵌入式软件工程技术研究中心上海200062 

出 版 物：《计算机工程》 (Computer Engineering)

年 卷 期：2019年第45卷第10期

页      面：70-77页

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家部委基金 

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

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