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

Formal Verification Framework of SCADE Model Based on STP Method

作　　者：林荣峰 施健[2] 朱晏庆 沈怡颹 周宇 LIN Rongfeng;SHI Jian;ZHU Yanqing;SHEN Yiwei;ZHOU Yu(Shanghai Institute of Spaceflight Control Technology,Shanghai 201108,China;National Trusted Embedded Software Engineering Technology Research Center,East China Normal University,Shanghai 200062,China)

机构地区：[1]上海航天控制技术研究所,上海201108 [2]华东师范大学国家可信嵌入式软件工程技术研究中心,上海200062

出　　处：《计算机工程》2019年第10期70-77,共8页Computer Engineering

基　　金：国家部委基金

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

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

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]