刍议面向航天器星载软件的形式化验证方法

发布时间：2021-11-16 09:18

　　随着星载软件在航天器上实现的功能比重越来越高,星载软件可靠性和可信性的指标要求越来越严格。传统软件测试方法的局限性难以确保万无一失,形式化方法以其高度数学化和严谨性的特点,常被应用于安全关键软件的验证。本文针对星载软件的高可靠性和充分性验证需求,初步提出了相应的形式化验证方案和需求建模实施过程,对于后续整星级的软件验证或者其他单机组件的验证具有一定的参考和借鉴意义。 

【文章来源】：电脑知识与技术. 2020,16(25)

【文章页数】：2 页

【部分图文】：

航天星载软件形式化验证技术方案

4 星载软件形式化需求建模实施过程在航天星载软件的形式化需求建模过程中，首先需要使用系统化的过程控制引导需求分析者逐步完成从需求文档到形式化模型转换。在形式化需求模型建立阶段，具体流程图2所示，具体来说有以下三步：

【参考文献】：
期刊论文
[1]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明.  软件学报. 2019(01)
[2]形式化验证在轨道交通领域的应用[J]. 于文涛.  电脑知识与技术. 2018(13)

硕士论文
[1]基于模型的软件需求验证方法研究[D]. 杜泽民.中国航天科技集团公司第一研究院 2018
[2]航天型号软件的安全性测试技术研究[D]. 马文姣.哈尔滨工业大学 2007



本文编号：3498586