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

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

Abstract: Design Verifier,the formal verification component of Safety Critical Application Development Environment(SCADE)can be used to verify the safety properties of embedded software systems in the aerospace field,but it cannot adequately describe the safety requirements of complex temporal properties.To solve this problem,a verification method of temporal properties for the SCADE state machine is constructed,which transforms the SCADE model into the NuSMV model.Linear Temporal Logic (LTL) and Computational Tree Logic (CTL) are introduced into the SCADE model requirements specification.Analysis results show that,with the aid of the NuSMV model checker as well as its verification results,complex temporal safety properties can be verified to reduce bugs at the requirements phase in the development cycle,and improve system security and reliability.

Key words: spacecraft system, formal verification, Safety Critical Application Development Environment(SCADE), safety-critical field, model checking, temporal properties

中图分类号: 

• TP31