计算机工程 ›› 2019, Vol. 45 ›› Issue (10): 70-77.doi: 10.19678/j.issn.1000-3428.0054411

• 体系结构与软件技术 • 上一篇    下一篇

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

林荣峰1, 施健2, 朱晏庆1, 沈怡颹1, 周宇1   

  1. 1. 上海航天控制技术研究所, 上海 201108;
    2. 华东师范大学 国家可信嵌入式软件工程技术研究中心, 上海 200062
  • 收稿日期:2019-03-28 修回日期:2019-05-14 出版日期:2019-10-15 发布日期:2019-07-12
  • 作者简介:林荣峰(1979-),男,高级工程师、硕士,主研方向为航天系统软件开发、可信软件技术;施健,硕士;朱晏庆,高级工程师、硕士;沈怡颹、周宇,工程师、硕士。
  • 基金项目:
    国家部委基金。

Formal Verification Framework of SCADE Model Based on STP Method

LIN Rongfeng1, SHI Jian2, ZHU Yanqing1, SHEN Yiwei1, ZHOU Yu1   

  1. 1. Shanghai Institute of Spaceflight Control Technology, Shanghai 201108, China;
    2. National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, China
  • Received:2019-03-28 Revised:2019-05-14 Online:2019-10-15 Published:2019-07-12

摘要: 高安全性应用开发环境(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

中图分类号: