面向适航标准的机载软件测试验证工具综述

刘友林，郑 巍，谭莉娟，樊 鑫，杨丰玉

1.南昌航空大学 软件学院，南昌330063 2.南昌航空大学 软件测评中心，南昌330063

机载软件是安装在航空设备中作为核心控制作用的计算机软件，是一种典型的嵌入式软件。随着嵌入式技术在航空航天领域的广泛应用，软件所实现的功能比例也越来越高，航电系统80%的功能都依赖于机载软件实现，机载软件已经成为机载设备系统的核心[1]，而因软件故障引起的事故时有发生。2018年印尼狮航因为飞机搭载的自动防失速系统做出错误判断导致空难。机载软件具有安全攸关（safety-critical）的特性，因此所有机载设备软件以及飞机交联的软件系统进行安全认证才能投入使用[2]。航空领域广泛采用的是美国航空无线电委员会（Radio Technical Commission for Aeronautics，RTCA）提出的航空适航认证标准DO-178C[3]及其增补标准。

基于适航认证标准的软件验证能最大程度上发现软件中的错误，保障软件安全与质量，满足适航审定的要求。机载嵌入式软件因其实时性、高安全可靠性和软硬件高耦合度等特点，验证的工作量和难度大大提升。如何对日渐复杂的机载软件系统进行高效的验证成为了研究热点，对机载嵌入式验证工具的研究同样也变得十分迫切。

DO-178C中软件验证的方法包括了审查（review）、测试和分析。而当前，国内外不少学者主要侧重于软件测试及其工具的研究。Sneha K等[4]按照功能导向将测试工具划分为功能测试工具、测试管理工具、负载测试工具三类；Mustafa K M等[5]根据测试工具的适用范围将其划分为web应用、嵌入式软件、数据库、网络协议等八类，但仅给出两种适用于嵌入式软件测试的工具。上述研究从不同角度对软件测试及其工具进行了研究，但是其主要研究对象并不是机载嵌入式软件，而且覆盖的工具也较少。因此本文在系列适航标准的基础上对机载软件的验证工具进行全面的研究综述。

DO-178C及其增补标准包括了工具鉴定（DO-330）、基于模型的开发和验证（DO-331）、面对对象技术（DO-332）、形式化方法（DO-333）、常温问题的问答（DO-248）等，如图1所示。面对对象技术（DO-332）到目前还没广泛应用到航空业中，工具鉴定（DO-330）是机载软件生命周期中所使用工具的适航审定标准，因此本文从DO-178C、模型驱动、形式化方法三个方面，介绍机载软件测试验证工具。

图1 适航认证标准

1 面向DO-178C的测试验证工具

DO-178C是民用航空机载软件研制和审定的指南标准，确保研制的软件实现预期的功能和满足适航的要求。DO-178C将软件生命周期分为软件计划过程、软件开发过程和软件综合过程，如图2。针对每个过程，DO-178C规定了一些系列的指南，包括过程的目标、达到目标所需要的活动和设计考虑、证明目的已经达到的证据。

图2 DO-178C软件生命周期

软件计划过程定义了软件计划和软件标准，用来指导软件开发和软件综合过程。软件开发过程实现了软件产品自上而下的生成。软件综合过程包含了验证软件产品、管理软件产品和监控软件产品，以保证软件产品及其生成过程的正确、受控和可信。软件综合过程中的软件验证过程不仅包含对软件开发过程的验证，还包括对软件验证过程输出结果的验证即对验证的验证。验证是对软件开发过程和软件验证过程结果的技术评估[3]。软件验证包括了评审（review）、分析、测试等方法，并通过不同的方法对不同的软件过程进行验证。DO-178C将测试作为软件验证的一部分考虑，主要是对开发出的源代码进行评估，执行测试用例以验证代码是否满足了需求。在软件需求不能用测试用例测试时，可以采用分析的方法验证。

1.1 评审

评审通过检查单或类似的方法进行人工定性检查，是早期发现问题的有效手段，通过评审可以发现其他方法难以发现的错误评。评审贯穿了软件研发的生命周期，包括软件需求、设计、代码、测试用例、配置项管理等过程。评审工具主要包括各阶段的评审检查单和生命周期数据等文档，设计合理充分的审查文档是保证评审质量的关键。

1.2 分析

软件分析可用于检查软件部件的功能、性能、安全性等，是可重复、可自动化的。软件分析的对象不仅仅是程序，还包括文档等其他形态的软件制品，如追踪性分析、源代码与目标代码的对应分析等。程序分析与形式化方法联系紧密，因此本文将其放在形式方法部分中归纳。

追踪性分析即在系统需求、高层需求、底层需求、代码、测试用例之间建立追踪关系，并对追踪关系进行分析。追踪性分析是为了确保需求测试的完整性，是软件验证活动的一部分，追踪关系和分析结果均需保存在验证报告中。软件需求阶段建立系统需求和软件高层需求间的链接，软件设计阶段建立高层需求和底层需求间的链接，软件编码阶段建立底层需求和代码间的链接，集成过程建立测试和需求、设计间的链接。工业界常使用IBM Engineering Requirements Management DOORS等需求管理工具，手动创建和维护追踪关系。该方法耗时长、成本高、维护较为困难。此外机载软件规模大、复杂度高，人工的追踪性分析不可避免地会存在问题。学术界对可追踪性的研究主要集中在追踪建立方法的研究上，并且大多数研究是在理论层面，基于相关理论的需求追踪工具的设计与实现是追踪性研究未来的主要工作之一[6]。

DO-178C（A7-9）指出机载软件需要进行源代码到目标代码的追溯分析，以确保源代码与目标代码的对应关系，保证编译器不会引入错误。源代码和目标代码对应分析最直接的方式是将源代码与目标码逐步对比分析，检测编译过程是否引入错误。但是该方法受软件研制过程影响大、分析成本高、工作量大。针对这种情况，上海爱韦讯提出了基于MISRA-2004的SCK-178语言安全子集，对安全子集内符合编码标准的参考代码进行了源代码与目标码的追溯分析，确保子集内的编码标准在编译环境不变的情况下不会引入错误。但是SCK-178安全子集尚无应用实例，其有效性存疑。

1.3 测试

DO-178C基于需求提出了三种测试方法：低层需求测试、软件集成测试、软件/硬件集成测试。低层需求测试主要测试软件是否满足底层需求。软件集成测试主要测试软件组件间的内部关系和软件体系结构。软件/硬件集成测试检查运行在目标机硬件上的软件是否满足需求，并排查目标硬件环境下可能出现的问题。DO-178C中的三种测试方法并不是自底向上、层层递进的关系，而是并列可选的关系即根据需求选择某种方法进行某项功能的测试。当系统需求比较简单，软件/硬件集成测试或者软件集成测试已经覆盖高层测试需求时，就没必要进行低层需求测试。

DO-178C还对测试的覆盖性也提出了要求，包括需求覆盖、软件结构覆盖。需求覆盖包括了高级测试需求和低级测试需求，软件结构覆盖包括了语句覆盖、判断覆盖、MC/DC覆盖、数据耦合和控制耦合，测试流程如图3所示。

图3 测试流程图

1.3.1 需求覆盖

需求覆盖最重要的部分是根据需求编写的测试用例。测试用例自动生成、测试用例复用、测试用例优化策略等技术一直在发展。文献[7]基于马尔可夫链定义系统模型并根据系统间状态转换的概率生成测试用例，系统间状态转换的概率会根据导致内存泄露的测试路径而迭代更新；文献[8]提出基于线性融合的用户协同过滤算法，有效地提高了测试用例推荐的精度，但是存在成本过高、泛化性等问题；文献[9]提出基于测试用例错误传播概率的测试用例优先级度量，根据该度量选择出的测试用例与Bug发现能力存在高相关性。但是根据软件需求人工编写测试用例仍是主要手段，相关技术与工具仅仅作为辅助。

1.3.2 结构覆盖

结构覆盖中的语句覆盖、判断覆盖、MC/DC覆盖是软件测试中自动化程度较高的部分，是软件测试工具主要的功能之一。本文结合DO-178C结构覆盖要求，选择了市场上主流且具有实际项目支撑的测试工具，包括了Testbed、Cantata等，并对其进行对比分析，如表1所示。

表1 测试覆盖工具

LDRA（Liverpool Data Research Associates）公司推出以Testbed为核心的测试套件，适用于软件开发、测试和维护等各个阶段。目前，国内各大航天航空企业、相关研究机构均已引进LDRA Testbed测试套件，作为主要的测试工具。北京航天自动控制研究所通过测试实例阐述Testbed在航空航天机载软件测试中的应用方案[10]；中航工业第一飞机设计研究院基于Testbed实现了机载航电系统综合数据记录系统的单元测试[11]。LDRA Testbed是第一个被用来证明空地系统符合DO-178B的工具，在机载软件测试领域拥有深厚的经验，且已占据我国机载软件测试工具主流市场，实际应用项目较多，工具可信度高。LDRA还可提供资质支持包来帮助客户通过DO-178B/C的认证。

Cantata[12]是QA SYSTEM公司研发的CC++代码的单元与集成测试工具，除了常规的代码覆盖率分析等功能外，还有健壮性测试、测试驱动开发等其他工具很少采用的测试方法和覆盖的功能。文献[13]以DO-178C为依据，通过规格化的用例设计方法生成测试用例，借助Cantata批量自动执行，发现的缺陷由13个增长至97个。

除此之外，还有Parasoft C/C++test[14]、VectorCAST[15]、Rapita Verification Suite[16]等测试工具，其综合性较强，其功能基本满足了DO-178C结构覆盖的要求，还涵盖了一些如时间性能分析、结构化分析等功能。但这些工具实际支撑项目较少，可信度未知。

1.3.3 耦合覆盖

耦合分析包括了数据耦合和控制耦合，DO-248C给出了数据耦合和控制耦合的示例[17]，以便理解，如图4所示。主函数调用了计算空速和空速显示子程序，计算出的空速作为全局变量在两个子程序间传递。主程序与子程序间存在控制耦合，子程序间存在数据耦合。耦合覆盖是结构覆盖中特殊的一项。DO-178B中明确提出了耦合覆盖的要求，DO-178C进一步强调了耦合覆盖的适航要求。但是适航标准中并没有给出明确的覆盖准则，甚至没有给出覆盖准则的指导思想。这使得耦合分析的开展比较困难，很难直接使用测试工具满足覆盖要求，需要综合评审、分析和测试的方法，流程如图5。

图4 数据耦合和控制耦合示例

LDRA Testbed提供了控制流和数据流分析的功能，也可用于耦合分析。SA-Covalyzer[18]是针对耦合覆盖分析研发的工具，自动识别部件间的耦合关系，推荐适用的覆盖准则，针对覆盖点进行低膨胀率的插桩，在测试过程中收集和统计覆盖情况，对未覆盖到的情形进行辅助分析，并自动生成覆盖分析报告。SA-Covalyzer是爱韦讯基于自身机载软件验证经验研制的工具，主观性较大，尚未实例，其可信度与实用性存疑。

图5 耦合分析流程

1.4 小结

国外嵌入式软件测试验证工具的研发起步早，一方面通过内部版本的迭代优化软件的功能，另一方面通过收购、合并其他公司和产品壮大自身，如开发CodeTest的AMC（Applied Microsystems Corporation）最后被并入恩智浦公司；研发Logicscope的Telelogic公司被IBM收购，其产品逐渐成熟，占据了主要市场甚至达到了垄断的地步。机载软件的测试验证工具作为一种工业软件，其研发在国内起步较晚，与国外仍有较大差距，发展水平与中国航空工业的发展速度不匹配。很多测试验证工具的实验性开发只能小范围落地使用甚至止步于实验室，缺乏用户的使用反馈数据，不利于相关的经验积累和技术积淀，无法对软件进行更好的优化，提高其综合竞争力。国产机载软件测试工具的发展落后存在多方面的原因。一是因为没有明确的政策导向，缺乏扶持和资金支持；二是国外主流的测试工具基本垄断了国内市场，国产的软件生存发展空间被压缩；三是国内工业软件相应的生态环境不成熟，用户没有使用国产机载测试工具的习惯。

2 面向模型驱动的测试验证工具

2011年RTCA发布的DO-178C，正式将模型驱动的概念引入航空航天领域，并增补标准DO-331[19]对基于模型的机载软件研发进行规范和指导。DO-331基于DO-178C，仅对采用模型的开发和验证的部分进行增加和修改。基于模型的验证方式主要是测试，因此本章侧重于基于模型的测试（Model-Based Testing，MBT）（图6）及其相应工具的研究。

图6 基于模型测试的流程

随着基于模型和以测试为中心的开发方法变得成熟，基于模型的测试也不断在发展。文献[20]梳理了近年来与MBT方法相关的文献，重点选取了78篇论文，详细分析了MBT方法的应用领域、特点和局限性等，比较的标准包括表示模型、支持工具、测试覆盖准则等。

基于模型的测试是测试的一种变体，其依赖于明确的行为模型，该行为模型可以对被测系统的预期行为或者其环境进行编码[21]。MBT提供一种使用从软件开发中提取的模型来自动生成测试用例的技术，以降低成本控制软件质量。大部分现有的MBT工具主要支持测试用例自动生成，可用于功能测试、性能测试和安全性测试等。借鉴文献[22]提出的分类方法，从建模方法的维度将MBT工具分为基于状态的建模、基于迁移的建模、基于统计概率的建模、基于数据流的建模。

2.1 基于状态的建模

基于状态建模的方法使用一组变量构建模型，该变量表示系统执行到特定点处的状态，包括了前置条件和后置条件。前置条件定义了初始状态集合，后置条件指定了最终可保证状态的集合。每个操作都指定为前置或者后置关系。状态建模的工具有Spec Explorer和基于Z语言的工具等。

Spec Explorer是微软研发的基于模型测试的工具，常使用Spec#或者C#作为描述系统模型的语言。Spec#在C#的基础上引入方法前置和后置条件、框架条件，对象不变式等形式化机制，并拓展了异常安全性、非空类型等用于提高程序可靠性的特性[23]。Spec Explorer对一个软件系统的期望行为进行建模，然后通过模型自动生成测试用例。模型可以用C#进行开发，然后通过Cord语言脚本对模型进行配置和裁剪，选择测试中需要的场景，因此Spec Explorer能有效解决状态爆炸的问题。文献[24]使用Spec Explorer工具进行测试，相较于手动测试，测试效率提高了42%。

Z语言是基于一阶谓词逻辑和集合论的形式规格说明语言[25]。Z语言具有一种特殊的图形方式（Scheme），主要由两部分组成：一是声明部分，定义各种变量的类型；另一个是谓词表达式。谓词表达式可以推理出所描述软件的所有状态行为。文献[26]给出了基于Z规格说明的测试用例自动生成的方法和框架。文献[27]研究了从Object-Z规格说明中产生测试用例的自动化过程，并在此基础上设计实现了相应的测试工具。Object-Z是在Z语言基础上增加了面对对象的封装和继承的描述能力。

2.2 基于迁移的建模

基于迁移建模的方法假设系统在某个时刻总处于某个状态并且当前的状态决定了系统可能的输入，而且从该状态迁移到其他状态的迁移决定于当前的输入。迁移建模对应的工具有TestMaster和基于统一建模语言（United Modeling Language，UML）的工具等。

TestMaster[28]基于扩展有限状态机来建立系统模型，并基于识别可迁移的输入序列来生成测试用例。每个生成的输入序列代表被测系统的一个测试用例，并且该工具还可以根据用户指定的路径覆盖方案生成测试用例。TestMaster使用基本图遍历算法的组合，如深度优先搜索、宽度优先搜索和最小生成树等，来导出EFSM的路径。

想想佛罗伦萨、巴黎、伦敦、纽约。第一次去这些城市的人也不会觉得它们陌生，因为他已经在绘画、小说、历史书和电影中去过这些地方了……格拉斯哥对我们多数人来说是什么？一所房子、工作的地方、足球或高尔夫球场、几家酒吧和纵横的街道。就这些。不，我错了，还有电影院和图书馆。……格拉斯哥在人们的印象中只是音乐厅里的一首歌和几本糟糕的小说。（Gray 2002：243；以下此书引用仅标注页码）格拉斯哥已经一无是处，等待它的只能是“死亡”。

基于UML的软件测试已经取得一定成果，包括基于UML各种图元的软件测试研究[29-31]、基于UML的软件可靠性测试与评估[32-33]等。文献[34]研制了基于UML的软件测试的工具Cow-Suite，该工具首先根据UIT（Use Interaction Testing）方法生成测试用例，再从生成的测试用例中选择合适的用例执行；文献[35]开发的验证性测试用例工具UMLTest，实现了对Rational Rose模型文件的解析，生成状态图并根据相应的测试准则产生测试用例；文献[36-37]定义了加入统计测试约束的UML用例图、序列图以及用例执行顺序关系的形式化描述，并在其基础上给出从UML模型构造马尔可夫链模型的算法，还设计实现了相关工具。

UML具有很好的面向对象性和丰富的建模表达能力，但是UML在非功能属性的表达上比较欠缺。基于UML的测试相关研究已经比较成熟，但是大多数集中于理论方面，对其相关工具的研发大幅度滞后，导致其使用门槛也居高不下，无法规模化地推广使用。

2.3 基于统计概率的建模

基于统计概率的建模对应的工具有MaTeLo Testing Tool（MTT），该工具使用马尔可夫链建模。马尔可夫链是一种以统计理论为基础的统计模型，其本质是一种具有概率特征的有限状态机，不仅可以根据状态间迁移概率自动产生测试用例，还可以分析测试结果，对软件性能指标和可靠性指标等进行度量。文献[38]利用缺陷关联信息扩展受控Markov链模型，以缺陷的三种属性作为决策选取权值，将测试过程看做带权最优路径求解问题，优化测试策略。

MTT是在MaTeLo[39]（Markov Test Logic）项目中开发的工具。该工具使用马尔可夫链建模，从被测软件的预期使用中生成测试用例。MTT关注的不是需求覆盖，而是覆盖被测软件的所有使用路径，以便检测使用中可能出现的关键故障。

2.4 基于数据流的建模

在基于模型的设计使用中，数据流模型是嵌入式系统中软件开发与测试中常用的模型。基于数据流模型的模型有Simulink Verification and Validation（SVAV）[40]和GAtel[41]。

SVAV提供包括IEC 61508等在内的行业规范的检查，还可以创建自定义检查标准。SVAV还可用于模型和代码覆盖率分析，以衡量模型和生成的代码的测试完整度。GAtel主要目的是根据以Luster语言编写的规范自动生成测试用例，Lustre是应用于关键应用程序的同步语言，具有语义形式化和模块化的特点。

2.5 小结

在对MBT的认知上，学术界与业界脱节较为严重。学术界对MBT研究比较广且深入，认为MBT已经成熟到可以较大规模应用，也开发了不少的原型工具投入使用，但是工业界不少测试从业者不了解MBT，MBT的商业化工具也仅有少量的研发，MBT在业界的应用仍处于起步状态。一是因为测试模型的选择、构建大多还是以经验为基础，且要求使用者具备建模语言、形式化方法等相关知识，知识储备要求高，建模自动化程度低，工具开发难度大，使用门槛高；二是MBT不支持安全性、可靠性以及性能等方面的测试，功能比较单一；三是MBT通常不能与软件开发环境集成，还缺少版本控制、模型试调等上下游工具链的支持。上述都是MBT科研成果向工业化、商业化产品转化过程中亟待克服的难题。

3 面向形式化方法的测试验证工具

形式化方法是一种建立在严格数学基础上的用于设计、规范和验证的方法，广泛地应用在软硬件、通信协议、嵌入式控制系统等方面[42]。DO-178C及其增补的DO-333首次正式将形式化方法引入到航空机载软件开发领域并确定了其有效性。文献[43]采用形式化方法对机载安全等级依赖的合法性进行了分析，文献[44]面向适航标准采用形式化方法对机载襟缝翼控制单元进行安全性分析。

形式化方法是由形式化语言、形式化规约、形式化验证等形成的整体[45]，其中形式验证的方法主要有模型检测、定理证明等。

3.1 模型检测

模型检测的基本思想是将一个过程或者系统抽象成有穷的状态模型，加以分析验证[46]。模型检测的自动化验证依赖于有效的软件工具的支持，本文选取了部分典型的模型检测工具SPIN[47]、UPPAAL[48]、CMBC[49]进行了对比，如表2所示。美国喷气推进实验室设计了SPIN模型检查器，对火星探测器的控制系统进行了验证[50]；文献[51]使用UPPAAL的衍生品UPPAAL-TRON对实时嵌入式系统进行黑盒一致性测试；文献[52]使用CBMC工具自动化验证程序覆盖率并应用在铁路系统中。除此之外还有很多模型检测工具被广泛地应用在软硬件的验证上，如SMV[53]、SLAM[54]等。

表2 模型检测工具

模型检测因为自动化程度相对较高，被广泛地应用在航空航天、轨道交通等领域。但是当模型检测在验证一些状态比较复杂的系统时，会出现空间爆炸的问题。目前，模型检测的主要研究方向就是如何减轻空间爆炸带来的影响。

3.2 定理证明

定理证明的基本思想是选定某个公理化系统，将验证的代码进行形式化描述为该系统的逻辑表述，利用公理与推理规则构造对程序的证明。本文选取了ACL2[55]和PVS[56]两个定理证明器进行了对比研究，如表3所示。

表3 定理证明工具

ACL2已被用来验证各种系统，如Sum公司的JAVA虚拟机系统，浮点单元、全真模拟系统等[57]；PVS被用于证明AAMP5处理器的正确性，该处理器被航空公司用于飞行控制[58]。定理证明工具还有Isabelle[59]、COQ[60]等。

定理证明可以有效地避免空间爆炸问题，但是因其自动化程度较低，对使用者的逻辑及数学知识储备要求较高，限制了定理证明在工业界的应用。目前，定理证明的研究方向主要是提高定理证明的自动化程度和自动化效率。

形式化验证还有抽象解释[61]、约束求解[62]、符号执行[63]等。

3.3 程序分析

软件分析是对软件进行自动化分析，以验证、确认或发现软件的某种性质、规约或者约束[64]。软件分析的对象不仅仅包括代码，还包括文档等其他形态的软件制品，本节软件分析所涉及的对象主要是程序。程序分析需要给出正确的程序不变性，而形式化验证只需要检查给定的程序不变性是否正确[65]。两者有严格的定义，但是在实际场景中混用比较多，文献[66]便将部分形式化验证方法作为程序分析的理论基础，如图7所示。

图7 主要程序分析技术

程序分析可分为静态分析技术和动态分析技术，而静态分析又包括基本分析技术、基于形式化的分析技术和其他分析技术[67]。

基本分析技术包括语法分析、类型分析、数据流分析、控制流分析等。基本分析技术发展比较成熟，应用也比较广泛。基于词法分析的ITS4、Rats，基于语义分析的PC-lint[68]，基于规则检查的Helix QACC++、Metal[69]，基于数据流分析的CppCheck、腾讯Tscancode，基于控制流分析和结构分析的Klocwork，基于规则检查和语义分析的北京关键科技EagleEye、Splint[70]，基于数据流分析和字节流分析的findbugs，基于数据流、控制流分析和代码结构分析的Fortify SCA等。

融合多技术进行代码验证是近年来的发展趋势之一，其中CPAchecker[71]是影响最为广泛的工具，该工具将模型检测与抽象解释进行结合。主流的软件安全分析与检测工具，如PolySpace、Coverity Prevent、CodeSonar等，基本都是多技术融合的产物。

具有独立自主知识产权的国产商业安全分析与缺陷检测工具的发展逐渐成熟，填补了我国缺陷检测、安全漏洞检测工具上的空白。CoBOT是北京大学软件工程中心研发团队打造的国内首款具有独立自主产权的代码安全类检测工具，打破了国外产品在软件缺陷检测和安全漏洞分析领域的垄断。SpecCheck是北京轩宇开发的缺陷检测工具，支持安全编码标准符合性检查、运行时缺陷检测和代码质量度量等。源伞科技的Pinpoint[72-73]是由香港科技大学孵化的一款商业化程度较高的静态缺陷分析工具，其服务对象覆盖了互联网、航天军工、通讯等行业。本文对上述软件安全分析与缺陷检测工具进行简要介绍与对比，如表4所示。

表4 安全分析与缺陷检测工具

3.4 小结

机载软件安全关键的特性要求从设计、需求到软件开发的每个阶段都要为机载软件的安全性与可靠性提供保证，测试与验证是其中的重要方法。当前测试仍是保证软件可靠性的主要且有效的手段，但是随着可靠性的增长，通过测试发现下一个bug的时间越来越长即可靠性增长相对于测试时间和代价是数量级。而在公理系统、验证工具正确的前提下，形式化方法能够严格保证软件符合其形式化规约。如果其形式化规约足够全面，则代码具有很高的可靠性。实际上，测试与验证往往是交错进行的。形式化方法对于提高软件质量的作用已经形成了共识，但是形式化方法的发展与应用同样存在困难。一是缺乏明确的规约或规格说明。大部分需求是非形式化描述的，并且分布在代码的各处。二是验证的粗粒度问题。粗粒度的验证会导致代码中仍存在bug，可靠性不高，细粒度的验证工作量大、成本高，并且非形式化的规约不好细化。

4 总结

本文按照适航标准系列文档，从DO-178C、基于模型的开发与验证、形式化方法的角度对工具的功能、特性及应用进行了详细介绍并对其发展现状进行小结。在对机载软件的测试与验证工具研究过程中，发现了以下问题并给出相应的建议。

（1）国产软件测试工具的竞争力弱，软件生命周期各个阶段的配套测试工具比较匮乏。具有独立知识产权且竞争力较强的测试工具，基本上是技术含量较低的缺陷管理工具、测试管理工具。国产自主化的功能性、安全性等方面的测试工具研发还处于起步状态，大部分市场份额被一些国外主流工具占据。缩小我国在工具研发等方面与国外之间差距，关键是加快建设国内科研-工业-商业的转化体系，在得到大量使用反馈之后优化测试验证工具，进一步提高国产测试验证工具的竞争力。

（2）大多数适用于机载软件测试的工具均支持国际民用航空适航标准DO-178B/C的验证，但是很少支持国内的标准，如GJB 2786A—2009（军用软件开发通用要求）、SJ 21141.1—2016（军用软件C/C++编程要求）、中国民航总局（CCAC）的CCAR 25.1309（民航设备、系统、安装方面的安全性要求）等。随着我国航空工业的发展，军用机载软件适航要求的提出和民用航空行业的开放，探索国际适航标准与我国军用、民用机载软件标准体系融合的方法、研发支持国际适航标准和国内标准的测试工具势在必行。

在对机载软件的测试验证工具研究过程中，还总结了一些关于机载软件测试验证及其工具研发的发展趋势。

（1）测试工具的集成化与一体化。单一化功能的测试工具以插件的形式集成到大型的测试工具中，一些市场上主流的测试工具被收购后集成到开发测试验证一体化的工具中，还有诸如DevOps、云测试等集成概念的提出以及实践，都反映了工具集一体化的趋势。不仅仅是测试工具，基本上所有的软件工具的研发都呈现集成化、一体化的趋势。

（2）人工智能与软件测试的融合发展更加紧密，智能化测试技术快速发展。基于深度神经网络的测试用例生成、软件缺陷预测与修复和基于知识图谱的测试用例推荐等都是智能化测试研究的热点。而人机交互智能的进一步发展，可能帮助计算机提高认知，实现从感知向认知演化，实现真正意义上的智能化自动测试。

（3）对适航标准中新增的形式方法和模型驱动技术的进一步研究。一方面，形式化方法与模型驱动工程的自动化研究及工具研发，能降低其使用门槛，提高易用性和扩展性，能够更好应用于保障机载软件的安全性与可靠性分析中；另一方面，人工智能技术与形式化方法交叉研究也是重要的课题，如基于神经网络的分析与验证、大数据程序的错误分析等。

（4）随着工具在机载软件研发过程中更加广泛的使用，为保障机载软件的安全性，针对工具的鉴定也会更加细化和严格。DO-178B仅将工具进行简单划分，并没有对工具鉴定有特定的要求。而DO-178C中不仅修订了工具类的划分，还给出了严格的审定认证条件，使得工具的鉴定更加客观。机载软件的不断演化和测试验证的实践中的反馈，使得工具鉴定的审定条件也不断在调整、更新。