航天嵌入式软件安全性验证技术  

The verification technology for aerospace embedded software safety

作　　者：高猛 王晓玲[1] 朱晓程 GAO Meng;WANG Xiaoling;ZHU Xiaocheng(Beijing Aerospace Automatic Control Institute,Beijing 100854,China)

机构地区：[1]北京航天自动控制研究所,北京100854

出　　处：《航天控制》2025年第2期72-78,共7页Aerospace Control

摘　　要：作为影响安全苛刻系统的重要因素,软件安全性问题日益受到关注。本文结合航天嵌入式软件工程实践,以软件安全性需求为线索,聚焦典型安全性问题,从源代码安全性质的形式化验证、软件安全性需求的自动化测试两个维度,分析总结了包括安全性专项分析、源代码静态分析、源代码模型检测、基于故障模型的安全性测试及关键字驱动的自动化测试等若干关键技术,提出了完整的航天嵌入式软件安全性验证的技术解决方案,研制了自主可控的软件保证支撑平台及工具,以系统提升航天嵌入式软件的可信保证能力。As a critical factor affecting safety-critical systems,it has been drawn increasingly attention to software safety issues.Based on engineering practices in aerospace embedded software testing and verification,the software safety requirements are taken as a clue and typical safety problems are focused in this paper.The two dimensions are introduced by the formal verification of source code safety properties and the automated testing of software safety requirements which analyze and summary key technologies,including special safety analysis,source code static analysis,source code model checking,fault-model-based safety testing and keyword-driven automated testing.A comprehensive technical solution for aerospace embedded software safety verification is proposed,and an independent controllable software assurance support platform and tools are developed to systematically enhance the trustworthy assurance capabilities of aerospace embedded software.

关 键 词：航天控制 嵌入式软件 中断驱动 软件安全性 形式化验证 自动化测试 

分 类 号：TP392[自动化与计算机技术—计算机应用技术]