王明亮 王永 尤志坚 施敏华

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

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

中图分类号：TP311文献标识码：A

文章编号：1009-3044（2020）25-0205-02

1概述

星載软件作为整个卫星的灵魂，由于实时性要求高、可靠性要求高、运行环境特殊、结构复杂等诸多特点，虽然经过单机对接测试、桌面联试、整星模飞等多种测试，但是始终面临需求分析严密性不足、测试充分性低下、逻辑设计错误等问题。特别地，传统航天软件以手工编码为主，随着软件规模和复杂度的提升，进度的压力使得保证需求分析和设计阶段的全面性十分困难[1]。传统测试方式难以从根本上改变和提高星载软件可靠性，为了提高软件质量，航天软件工作者不停地在多个层面积极开展工作确保万无一失，如制定并实施一系列航天软件工程标准和规范、积极推进基于GJB5000A的软件过程改进、对软件进行大量的测试（单元测试、组装测试、确认测试、系统测试、整星测试等）验证尽可能多地暴露软件问题，这些方法极大地减少了软件错误的数量，保证了航天任务的成功。但尽管如此，软件中的一些深层次的缺陷问题并不能在软件测试中被全部识别，亟须采用更为严格的数学逻辑推理即形式化验证的方法来提升和确保软件的可靠度。

2形式化方法研究动态

形式化验证通过对系统进行穷尽搜索来进行验证，它以某个或某些形式的规范或属性为依据，使用数学的方法证明其正确性[2]。Robert W. Floyd于1967年提出的最早的形式化方法之一公理化方法验证程序的控制流，以及随后TonyHoare在此基础上继续研究于1969年提出了程序验证的公理系统Hoare逻辑;陈钢博士在2016年3月的北京大学学报上发表了综述性的文章对基于逻辑的各种形式化验证方法和工具进行分析比较，可以帮助工程师从应用角度选择使用验证工具。清华大学贺飞博士等在软件学报上开辟了软件形式化验证和形式化方法理论基础专题，对最新录用的国内外研究论文进行评价分析;丁明等提出了业务流程上的形式化设计和验证方法;针对应答器报文编制规则黄旭等人给出了形式化建模与验证方法;赵正旭等在2016年进行的Z规格说明的推理与验证;查君鹏针对SPARCv8汇编程序进行了形式化验证;部分图灵奖获得者也在形式化方面进行了一些研究工作，如下表所示[3]。

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

形式化方法是一种以数学基础为设计理念，针对数字化系统进行规格说明撰写、软件开发、软件验证的技术，数学基础包括形式逻辑，离散数学和机器可识别语言等。形式化模型是一种用数学语法和语义刻画的模型，是一种对软件诸多方面的抽象表达形式，用于后续的分析与验证。应用形式化验证方法的前提条件是对即将开发的软件工程建立一个形式化全周期模型。

针对航天星载软件的形式化验证，首先要根据卫星分系统技术需求文档建立形式化需求模型，然后对其进行分析与验证，从而在软件开发的早期发现并解决需求中存在的问题，诸如可达性错误，数据溢出超限，量纲错误，二义性错误等。基于验证过的需求模型将其转化为系统模型，在模型中验证系统是否符合给定的安全性质，如顺序性，完备性等。同时，利用模型动态检查技术，在模型模拟执行时定位并发现代运行时错误，如并发性竞争等时序错误。针对验证过的系统模型可以自动生成软件代码，但是因为现有的航天软件大部分情况下均已存在经过严格测试的软件代码，一般不会直接使用生成的代码，而是作为原有代码的参考补充。同时，基于模型可以生成相对应的测试用例用于测试代码，保障代码的可靠性与安全性。星载软件形式化验证总体方案如图1所示。

4 星载软件形式化需求建模实施过程

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

1）根据航天领域的特征提取系统功能和行为特征，给出需求模板背后的形式化语法和语义，制定对应的需求模板。

2）根据需求模板，将原有的自然语言撰写的非形式化需求文档按照填充到模板中形成形式化需求文档。填充模板的好处是不需要工程师学习形式化的数学语义便可以完成需求文档的形式化转换，其原有的工作流程不会受到影响。同时，在该过程中分析提取系统所需要验证的安全性和可靠性性质，为后续的性质验证提供输入。

3）将形式化需求文档作为工具的输入，机器自动将其中的自然语言等非形式化内容全部过滤去除，得到由纯形式化语言描述的需求模型，我们称之为软件的“原型”。

软件需求分析位于软件开发的前期，是软件生存期中重要的一步[4]。由于在软件起步阶段，人们对系统预期功能尚不明确，而参与系统分析的人员背景不同，因此，采用自然语言完成初始的需求文档显然是个合理的方式。特别是对于航天星载软件的需求来说，需求分析人员需要频繁地与委托方进行方沟通交流，基于自然语言的非形式化需求规约在这个阶段比形式化需求规约在可读性和可理解性上有明显的优势。

5 结束语

形式化验证在自顶向下的实现流程中增强了设计人员对系统的理解，能够发现其他方法不易识别的设计缺陷，揭示系统设计中存在的不一致性、模糊和不完整性等问题。正如1996年IEEE会刊提出的观点：“随着软件设计复杂度的不断提高，形式化验证将从实验室走进生产领域”。形式化验证理论研究虽然在学术上取得了一定成功，但是在工程落地方面还有很长的路要走。因为对于一般的软件测试人员，在理解形式化推理演绎技术前，要先研究相对难度较高的形式化相关基础数学推演理论，再尝试将系统转换为形式化模型形式化应用，带来过高人力成本和难以接受的测试周期。但是，作为面向软件正确性证明的最严格的基础数学方法，软件形式化验证对软件测试可信度和充分性的提升是毋庸置疑的。

参考文献：

[1] 杜泽民.基于模型的软件需求验证方法研究[D].北京： 中国航天科技集团公司第一研究院， 2018.

[2] 于文涛.形式化验证在轨道交通领域的应用[J].电脑知识与技术.2018，14（13）：263.

[3] 王戟、詹乃军、冯新宇、刘志明.形式化方法概貌[J].软件学报， 2019，30（1）： 33-61.

[4] 马文姣. 航天型号软件的安全性测试技术研究[D].哈尔滨： 哈尔滨工业大学， 2007.

【通联编辑：梁书】