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

作　　者：王明亮 王永[2] 尤志坚 施敏华 

机构地区：[1]中国科学院微小卫星创新研究院,上海201203 [2]上海微小卫星工程中心,上海201200

出　　处：《电脑知识与技术》2020年第25期205-206,共2页Computer Knowledge and Technology

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

关 键 词：星载软件 形式化验证 需求规约化 形式化语法 

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