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

摘要

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