面向DO-178C软件测试过程的目标符合性论证模式

杨 阳 吴 际 苑春春 刘 超 杨海燕 邢 亮

1(北京航空航天大学计算机学院 北京 100191)2 (中航工业西安航空计算技术研究所 西安 710068) (yyangbuaa@sina.com)

面向DO-178C软件测试过程的目标符合性论证模式

杨 阳1吴 际1苑春春1刘 超1杨海燕1邢 亮2

1(北京航空航天大学计算机学院 北京 100191)2(中航工业西安航空计算技术研究所 西安 710068) (yyangbuaa@sina.com)

安全关键软件已广泛应用于众多领域.鉴于其对防范灾害风险方面的特殊要求，必须符合相关领域的安全性标准.但是目前对于如何建立面向标准的目标符合性论证模型，尚缺乏有效的方法.针对DO-178C标准中关于软件测试过程目标的特征描述，提出了一个基于GSN的目标论证模式描述框架，分别从解决问题、解决方案、应用方法和产生效果4个方面对目标论证模式进行描述；同时使用一种扩展的安全案例模式描述方式，用以描述面向标准的目标符合性论证模式.在此基础上，提出了3种面向DO-178C软件测试过程的目标符合性论证模式，分别是代码-需求符合性论证模式、需求测试覆盖率论证模式、结构测试覆盖率论证模式，并提出基于这些模式建立针对特定项目的目标符合性论证结构的实例化方法，为建立面向DO-178C软件测试过程的目标符合性论证结构提供了有效指导.通过一个机载嵌入式实时操作系统的案例，说明了提出的目标符合性论证模式的可用性和有效性.

安全关键性软件；适航认证；DO-178C；GSN；论证模式

安全关键软件(safety critical software)正在越来越广泛地应用于航空、航天、高铁、汽车、能源、通信、医疗、金融、工业控制等众多领域.这类软件必须符合各自领域中规定的安全性相关标准，比如在航空领域，机载软件必须符合最新的适航审定标准DO-178C[1]以及一系列相关标准，并通过局方的适航审定，才能投入使用.DO-178C针对不同安全等级的软件分别提出了一系列目标，比如A级软件必需满足全部71个目标，其中针对A级软件的单元测试，要求必需满足语句覆盖、分支覆盖和MCDC覆盖等测试充分性准则.机载软件的开发方需要依据软件开发过程中产生的各种数据和信息，提供必要证据，通过有效的论证过程说明其符合安全性标准中规定的目标.

但是，目前在建立面向标准的目标符合性论证结构方面还存在3个基本问题：

1) 建立面向特定项目的论证结构涉及的因素多且建立过程复杂.安全性相关标准中对产品开发过程及其制品以及相关影响因素的监控等均有严格的要求，明确规定了必须满足的一系列目标，包括蕴含的相关子目标和具体要求.为了对特定的安全关键软件或系统的标准符合性进行有效论证，需要将其开发过程(包括各种相关活动及其采用的方法、准则、策略以及实际执行结果中可提取的安全性相关证据等)与相关标准的具体目标和要求之间建立起明确的关联.因此，需要依据相关标准，建立针对具体项目的安全性论证结构，以支持其安全论证体系的建设、安全性相关证据的采集和分析以及安全性目标的论证.然而，如何从标准中提取出必需满足的各个目标及其相关子目标和具体要求，以建立安全性论证结构，以及如何建立其与具体项目过程及其所产生的相关证据之间的关联，目前尚没有有效的方法.

2) 对于不同的软件项目，由于其产品特点和开发过程等方面的差异，其论证结构之间亦存在差异，致使项目相关的论证结构难以重用.但是，由于在相关标准的约束下这些论证结构之间显然存在高度的相似性，因此有必要提炼共性特征，以方便论证结构的快速建立.例如提炼具有共性的论证结构模式，并据此自动生成针对项目的特定论证结构实例.

3) 事实上，安全性相关标准中规定的各种目标之间存在一定关联，其符合性论证结构之间也存在一定的相似性，因此可以进一步提炼面向不同目标的论证结构模式.

本文以DO-178C规定的软件测试过程目标为研究对象，参考安全案例模式(safety case pattern)[2]，将可重用的结构模式引入到目标符合性论证结构设计中，提出了3种针对软件测试过程目标符合性论证结构的论证模式，以及通过对论证模式的实例化建立面向项目的论证结构的方法.并以某实际项目为应用案例，说明本文提出的目标符合性论证模式的可重用性和有效性.这种基于模式的目标符合性论证方法，对于其他面向标准的目标符合性论证同样具有参考价值，适用于针对DO-178C等安全性相关标准的目标符合性论证结构的建立.

1 适航软件论证研究现状

1.1 DO-178C标准

DO-178C[1]依据软件失效带来的危害等级，将软件分为A，B，C，D，E五个级别.其中A级软件对安全性要求最高，E级软件则不需要满足DO-178C标准中规定的目标.DO-178C规定了不同安全等级的机载软件在软件开发过程中必须符合的目标和相关要求，在机载软件的安全性认证中已被广泛采用.NASA的研究员Holloway[3-4]对于DO-178C中提出的总目标与软件开发过程中需要达到的各个目标之间的证明与被证明关系进行了分析，并通过对这些目标的分类，利用GSN(goal structuring notation)[5]清楚地展示了针对不同安全等级的软件，其过程目标与总目标之间的结构关系.国内也有针对DO-178BC的研究，文献[6]将DO-178B标准与DO-178C标准进行比较，分析了DO-178C在软件开发过程中新增或者变更的内容；文献[7]提出了满足DO-178B中结构覆盖率分析的解决方案，并在实际的项目中应用.

在基于DO-178C的认证方面，软件审批指南(software approval guidelines)[8]为基于DO-178C的认证提供了指导，该指南指出在执行基于DO-178C标准的认证时应该考虑的因素，并得到了广泛认可.

1.2 软件的标准符合性论证方法

标准符合性论证指的是通过建立一种规范的论证结构来支持对项目实施过程是否符合标准的论证.论证结构中通常包括待论证的标准目标、结构化的论证过程以及用来论证目标的数据或证据.

为了论证软件是否符合标准中规定的目标(如软件测试过程需满足的目标)，可以使用不同的论证方法.例如基于检查单的论证、基于GQM[9](goal question metric)模型的论证、基于GSN[5]模型的论证等.

基于检查单的论证是在工程实践中常用的方法[10].这种方法将标准中规定目标的具体要求以检查单的形式列举出来，通过人工检查来确认被论证的软件是否符合检查单中规定的各项要求.这种论证方法不仅工作量大，更重要的是通用的检查单中无法体现具体项目的特点和差异，且无法建立目标与证据之间的关联，论证结果常会受到论证人的主观判断的影响.

GQM是一种层次化的论证方法，以表格的形式表达，分为目标、问题和度量3层.首先确立目标，然后将目标分解成若干问题，并针对每个问题采用量化的度量来进行论证.然而，这种固定的3层结构对复杂目标的分层细化难度很大，因此无法支持针对DO-178C这类标准的严谨论证.此外，在度量层，只考察了预定的度量数据，而不考虑各种复杂数据或证据之间的关系，以及开发人员能力等复杂的影响因素.因此，GQM也具有明显的局限性.

GSN[11]是一种结构化的表示论证组织形式的方法，其主要论证结构为：总目标、可分层细化的子目标及其分解策略、子目标对应的证据.基于GSN的论证指的是针对每个待论证的目标，建立对应的GSN结构，并根据采集到的证据进行目标论证的方法.GSN是一种多层的论证结构，可以根据标准对目标的定义和相关要求，将目标分解为若干个子目标，并可以准确描述目标的分解策略等，为目标论证提供必要依据和指导.此外，图形化的表达方式使得复杂的论证结构更加直观，易于理解.在GSN基础上，GSN提出者通过文献[11]从论证模式和模块化表示2个方向进行扩展，使得GSN的适用范围更加广阔.

除了GSN提出者的研究团队，其他的研究团队针对GSN模型也从不同的侧重点进行了扩展.Takai等人[12]提出在安全案例发生变更时，针对变更的表示方法，并通过案例说明了该方法的有效性.Matsuno等人[13]提出了基于GSN的安全案例模式的一种参数化表达方法，这种方法可以支持一致性检查，避免使用安全案例模式进行参数实例化时出现的一致性错误.

1.3 安全案例和安全案例模式

安全案例用来论证在特定的上下文中，系统是否具有足够安全的保证[2].安全案例是一种论证结构，由论证目标、结构化的论证过程以及证据组成.依据证据，通过结构化的论证过程来论证预期的目标是否成立.目前，通常使用GSN来表示安全案例.

安全案例模式(safety case pattern)[2]的概念是由Kelly和McDermid在1998年提出的.安全案例模式使用GSN表示，并对GSN的符号进行了一定的扩展.安全案例模式将可复用的论证结构这个概念引入了安全案例中.在此基础上，Alexander等人[14]依据建立安全案例的经验，在2007年发表1份报告，针对先进控制软件总结了14种安全案例模式，并且使用了参数化的表示方法来描述安全案例模式，为建立该类型软件的安全案例提供了指导.

2 基于GSN的目标论证模式框架

本文提出一种基于GSN的目标论证模式描述框架，分别从模式的解决问题、解决方案、应用方法和产生效果4个方面对目标论证模式进行描述，并提出了一种扩展的安全案例模式描述方式，用于在解决方案中详细定义面向标准的目标符合性论证模式.该描述方式针对安全案例模式进行扩展，下面对安全案例模式的主要结构和本文扩展的部分进行介绍.

安全案例模式的主要结构如下.

1) 主要论证元素：目标(矩形框表示)、策略(平行四边形表示)、证据(圆形表示)；辅助论证元素：上下文(圆角矩形框表示)、假设(右下角有大写字母A的椭圆形框)、论证(右下角有大写字母J的椭圆形框)；关联关系：实心箭头建立主要论证元素之间的关联、空心箭头建立主要论证元素和辅助论证元素的关联.

2) 在目标和策略中引入模式变量(以下简称变量)，用{变量名}表示，并在其关联的上下文中对变量进行进一步解释说明，包括对其值域的定义，表达方式为

变量名: {值，…}.

这些变量可以指代目标论证所针对的软件(项目)、待论证的性质或要求、相关的活动或制品、候选策略、环境约束等.此外，定义#(Y)为集合Y中元素的数量.

3) 扩展的关联关系.在关联关系上增加了对实例化数量的约束，用“带实心圆点的实心箭头+实例化后的目标数量”表示；目标间“或”的关联关系，用“实心箭头+菱形”表示.

本文扩展的部分如下.

1) 目标关联的上下文中定义目标约束条件.含义为：在进行论证模式实例化时，只有约束条件成立时，对应的目标才会存在.

2) 证据关联的上下文中必须定义对证据结构的要求，只有提供的证据元素符合结构的要求时，才能保证最终建立的论证结构成立，可以进行论证推导.

3) 建立与标准的关联.在各类节点中，用“(标准中相关条目编号或章节号)”方式注释其与标准中相关条目的关联性，方便检查核对论证结构与标准的对应关系.

4) 添加含有字母T的矩形框，用于目标下方.表示该目标成立，不需要用证据证明.

Fig. 1 Code-requirement conformity argument pattern 1图1 代码-需求符合性模式1

为了清晰地区分出图1～8定义的各种元素，图1～8各个元素的标识符均使用大一号的字号；标准的关联性注释使用带下划线的字；所有变量名均使用斜体字.上述扩展元素的标识方式，参见第3节.

此外，本文使用的复合目标，该符号源于文献[11]对GSN的扩展.复合目标(类似文件夹的图形表示符号，并在其中填写名称)，其本身是一个独立的论证结构.引入复合目标，是为了提取可重用的论证结构，避免在多个目标论证中对其进行重复定义.同时，通过对复合目标的引用，可以简化复杂的论证结构.

3 面向DO -178C软件测试过程的论证模式

通过对DO-178C标准中关于软件测试过程目标和相关要求的分析，本文提出了针对此类过程的3种典型的论证模式，实现了其目标符合性论证结构的可重用性.这种可重用性主要体现在2个层面：

1) 这种模式可以表示面向标准(即独立于特定项目)的目标符合性论证结构；

2) 这种模式可以表示针对1个项目中多个同类目标的符合性论证结构.

3.1 代码-需求符合性论证模式

3.1.1 解决问题

DO-178C规定的基于需求的测试活动的主要目标是测试可运行目标代码与需求之间是否符合、是否健壮.本节中提出的模式为建立目标代码与高层需求和低层需求之间的符合性与健壮性目标(DO-178C附录A中表A-6的目标1～4)的论证结构提供具体指导，并可通过实例化该论证模式，进一步建立针对具体项目的论证结构.

3.1.2 解决方案

解决方案如图1和图2所示.

Fig. 2 Code-requirement conformity argument pattern 2图2 代码-需求符合性模式2

图1描述了DO-178C规定的基于需求的测试活动的主要目标，包括测试可运行目标代码与需求之间符合性(compliance)和健壮性(robustness).图2是对复合目标G2的定义.在该模式定义中：

1) 目标G1中引用的模式变量S指代软件名称，在实例化时可直接使用具体的软件名称替代；X的取值是其上下文描述中定义的complies或is robust；Y的取值是high-level requirements(高层需求)或low-level requirements(低层需求).

2) 在上下文元素中分别定义了其对应的目标或策略的约束条件.例如对策略S1，当G1针对的是Y=high-level requirements时，要求论证T=hardwaresoftware integration testing(硬件软件集成测试)的实现；否则，当Y=low-level requirements时，则应论证T=software integration testing and low-level test(软件集成测试以及低层测试).类似地，对目标G2，如果G1针对的是X=complies，则G2中的Z=normal range(测试正常范围)，否则Z=robustness(测试鲁棒性).而对于目标G8，则规定只有当需求中包括状态转换的内容时，其才需要存在.

3) 针对证据的上下文描述中给出了对证据结构的要求.例如对于证据E1，其上下文描述中定义了测试用例中应该包含哪些元素，只有提供的证据元素符合上下文描述中对证据结构提出的要求时，才能保证最终建立的论证结构是成立的，可以进行论证推导.

图1和图2所示的模式表达了DO-178C标准附录A中表A-6的目标1～4的论证结构，分别用于论证可运行目标代码与高层需求或低层需求之间的符合性及健壮性.针对总目标G1(可运行目标代码和需求之间的符合性或健壮性)的论证，被分成2个论证结构，即测试用例的选择符合标准定义的规则(S1→G2)以及对整个测试活动中追溯性的检验(S2→{G3,G4,G5}).论证1结构依据S1进行分解论证，S1说明编写的测试用例所属测试类型，分解到G2目标，描述了针对各项具体需求编写覆盖正常范围(或健壮性)的测试用例集，并通过扩展的关联关系说明在实例化论证模式时，要求实现n个目标G2，其中n为需求的总数量(n=#(Y))，即变量R将实例化为一项具体需求，并且对应每一项需求都将实例化出一个G2的实例.在图2中，将G2按照策略S3向下分解，通过G6～G13将不同类型的需求(时间相关的需求、涉及到状态转换的需求、包含整型实型的需求)，在不同条件下(正常范围内的测试或者健壮性测试)需要选择的测试用例的目标分别表示出来，并且每个目标的约束条件都以其上下文描述的形式给出定义，最终这些目标用证据E1论证目标是否实现.论证2结构依据S2进行分解论证，判断需求、测试用例、测试程序、测试结果之间是否存在追溯性.其中，目标G3表达每个需求都至少存在一个测试用例，目标G4表达每个测试用例都由测试程序实现，目标G5表达每个测试程序都有测试结果，最终用证据E2论证这些目标是否实现.此外，对证据E1，E2的结构要求定义在其对应的上下文描述中.

3.1.3 应用方法

实例化模式的方法分为5步:

1) 结合项目真实情况实例化论证模式中的模式变量，即将其赋值，并将模式中定义模式变量可能取值的上下文描述矩形框删除.

2) 结合项目实际情况判断是否满足上下文描述中定义的约束条件，删除不符合约束条件的子目标及其约束条件，并且在保留的子目标中，将对应的约束条件保留，并以假设(右下角有大写字母A的椭圆形框)的形式作为辅助论证结构来支撑对应的子目标，其含义是：当这个假设成立时，对应的子目标才可以进行是否成立的论证.

3) 项目中实际的证据结构必须满足模式中规定的证据结构，否则无法进行目标符合性论证.

4) 依据项目实际情况，可以对现有的目标进行进一步的分解，或者添加原来模式中没有但是项目中必需的子目标项，提供对应证据，并给出对证据结构的要求，以上下文描述的形式与对应证据相关联.

5) 检查最终实例化目标论证结构，最终建立的论证结构中，不能包括未实例化的模式变量；除证据结构要求的上下文描述项，不能包含其他约束条件上下文描述项；如果没有达到上述条件，则重复上述步骤继续实例化.

本文以1个简化的嵌入式实时操作系统(本文中称作操作系统A)的论证目标DO-178C附录A中表A-6的目标1为例，采用上述方法，通过实例化上述论证模式，建立了该项目中针对该目标的论证结构，如图3所示.

图3中，首先对G1进行实例化，说明论证的总目标是操作系统A中可运行目标代码和高层需求之间的符合性，并在其上下文描述对A进行说明.依据策略S1，S2将总目标G1向下分解.

1) 实例化策略S1的论证结构，编写高层需求的测试用例属于软件硬件集成测试.实例化图1中的目标G2，该软件存在9项高层需求，实例化为图3中的目标G2.1～G2.9.G2.1描述了操作系统A中任务挂起需求的测试用例要求，按照本模式中的定义，这个需求属于状态转换需求，对应于图2中的G8，除此之外，该需求不满足这一层级其他目标的约束条件，因此对于这个目标来说，实例化时将删除模式中的目标G6，G7，G9，G10，G11，G12，G13，只保留G8，并将G8中的约束条件转换为图3中目标G3.1相关联的假设(右下方有大写字母A的椭圆形)，保留模式中的G8被实例化为图3中G3.1，来测试正常操作下所有状态转换.依据操作系统A的特点可以知道，当任务处于就绪态或者休眠态，并且任务中没有锁(锁机制是操作系统中保持数据一致性的一种机制，文献[15]介绍了操作系统中锁的实现原理)时可以挂起，因此在该模式的基础上，还需要添加目标G4.1和目标G4.2，并通过证据E1证明是否符合目标.

Fig. 3 An example of code-high-level requirement conformity argument structure图3 代码-高层需求符合性论证结构示例

由于篇幅限制，本文没有将G2.2～G2.9的所有目标列举出来，使用省略号表示，此外G2.9目标下的菱形框表示这个目标需要进一步分解.

2) 实例化策略S2的论证结构.图1中的目标G3要求每个需求都要存在至少一个测试用例.为了节省篇幅，图3没有将每个具体需求的编号逐一展示，而使用“Every requirement has”(每个需求都要实现)这样的句型表示.图1中的目标G4和G5实例化情况类似.因此，图1中的G3，G4，G5目标分别对应于图3的G2.10，G2.11，G2.12，并通过证据E2证明是否符合目标.

3.1.4 产生效果

建立代码-需求符合性论证模式，有助于为不同项目实现DO-178C附录A中表A-6的目标1～4的论证结构提供便利.论证模式包含了DO-178C针对这些目标规定的需要执行的所有活动，即在该模式中标注了标准中规定的所有相关活动，因此最终建立的论证模型符合标准规定，并可通过规范的步骤实例化，从而最终建立简明的论证结构.

此外，模式中为不同活动的执行规定了约束条件，因此，可以依据项目的实际情况决定是否执行该活动，对标准中规定的活动是否执行提供了指导，在保证符合标准的前提下最大程度地提高了效率，避免执行不必要的活动.

3.2 需求测试覆盖率论证模式

3.2.1 解决问题

DO-178C规定的基于需求的测试活动需要验证需求的测试覆盖率.本节中提出的模式为建立需求测试覆盖率目标(DO-178C附录A中表A-7的目标3～4)的论证结构提供具体指导，并可通过实例化该论证模式，进一步建立针对具体项目的论证结构.

3.2.2 解决方案

解决方案如图4所示：

Fig. 4 Test coverage of requirements argument pattern图4 需求测试覆盖率论证模式

Fig. 5 An example of test coverage of requirements argument structure图5 需求测试覆盖率论证结构示例

图4描述了针对DO-178C附录A中表A-7的目标3～4的论证模式，分别用于论证高层需求和低层需求的测试覆盖率.论证目标G1，分成3个子论证结构，即论证测试用例覆盖了所有需求，论证所有的测试活动都是基于需求的，论证整个覆盖率分析所执行活动的过程中发现的缺陷都记录并且解决了.论证1结构依据S1进一步分解为目标G2，G2又分解为目标G6和G7.G6验证基于需求的测试用例是否满足规定的正常以及健壮性测试准则，用验证结果E1论证该目标是否实现.G7说明每个需求都存在正常和健壮性测试用例，用测试用例E2和追溯数据E3论证该目标是否实现.论证2结构依据S2分解为G3和G4，分别说明每个测试用例可以追溯到需求和必须存在测试程序可以追溯到测试用例.通过这2个目标来说明所有测试活动都是基于需求的，用追溯数据E3论证该目标是否实现.论证3结构依据S3分解为G5，说明所有发现的缺陷都被记录并解决，用问题报告E4论证该目标是否实现.其中对证据E1，E2，E3，E4的结构要求定义在其对应的上下文中.

3.2.3 应用方法

实例化的步骤与3.1.3节应用方法中的1，3，4，5一致，因为本模式中不存在需要删除的子目标，也不能删除任何子目标.即便在需求测试覆盖率分析过程中没有发现错误，G5中的模式变量D可以用null表示，但是G5是DO-178C中规定必须执行的活动，因此不能删除.

同样以操作系统A为例，采用上述方法实例化论证模式建立了针对DO-178C附录A中表A-7的目标3的论证结构，如图5所示.

Fig. 6 Test coverage of structure argument pattern 1图6 结构测试覆盖率论证模式 1

图5中，先对G1进行实例化，说明论证的总目标是高层需求的测试覆盖率符合标准.依据模式中定义的策略S1，S2，S3将总目标G1向下分解：

1) 实例化策略S1的论证结构.即论证测试用例覆盖了所有的高层需求，实例化图4中的目标G2，得到图5中的目标G2.1～G2.9，其中G2.1描述了操作系统A中任务挂起需求需要被测试用例覆盖，G3.1说明该测试用例要满足标准中的准则.依据DO-178C中对建立测试用例准则的描述，针对该需求需要建立正常操作以及异常操作下所有可能产生的状态转换的测试用例，因此添加目标G4.1来说明，判定是否建立了这样的测试用例集，并通过证据E1来验证.除此之外，还需要说明需求包含正常测试用例以及健壮性测试用例，在目标G3.2中说明，并通过证据E2和E3证明是否符合这项目标.

同样篇幅限制，本文没有将G2.2～G2.9的所有目标列举出来，使用省略号表示.

2) 实例化策略S2的论证结构.图4模式中G3目标要求每个测试用例都可以追溯到需求.为了节省篇幅，实例化时图5没有将每个具体的测试用例的编号逐一展示，而使用“Every test case is”(每个测试用例都要实现)这个句型表示.图4中的目标G4实例化时情况类似.因此，图4中G3，G4目标分别对应于图5的G2.10，G2.11，并通过证据E3论证是否符合目标.

3) 实例化策略S3的论证结构.在本例中由于没有在论证需求的测试覆盖率所执行的活动过程中发现错误，因此在子目标G2.12下添加含有内容T的矩形框，表示其自动成立，不需要通过证据证明.

3.2.4 产生效果

建立需求测试覆盖率论证模式，有助于对不同项目实现DO-178C附录A中表A-7的目标3～4的论证结构提供便利.论证模式包含了DO-178C针对这些目标规定的需要执行的所有活动，即在该模式中标注了标准中规定的所有相关活动，并且在标准规定的基础上，对实现这些活动的途径进行了扩展，因此最终建立的论证模型不仅符合标准规定，而且具有可行性，并可通过规范的步骤实例化，从而最终建立简明的论证结构.需要注意的是，本模式中所有的子目标都必须包含并进行论证，否则将不满足标准的规定.

3.3 结构测试覆盖率论证模式

3.3.1 解决问题

DO-178C规定的基于需求的测试活动需要验证结构测试覆盖率.本节中提出的模式为结构测试覆盖率目标(DO-178C附录A中表A-7的目标5～7)的论证结构提供具体指导，并可通过实例化该论证模式，进一步建立针对具体项目的论证结构.

Fig. 7 Test coverage of structure argument pattern 2图7 结构测试覆盖率论证模式 2

3.3.2 解决方案

图6和图7描述的是针对DO-178C附录A中表A-7的目标5～7的论证模式，分别用于语句覆盖率、分支覆盖率以及MCDC覆盖率.论证目标G1分成3个论证结构：1)当待论证软件是A级软件时，需要验证额外代码[1](即由编译器、链接器或者其他方式生成的不能直接追溯到源代码语句的代码)；2)论证代码的结构化覆盖率；3)论证整个覆盖率分析过程所执行的活动中发现的缺陷都记录并且解决.论证1结构的论证目标是G2(与DO-178C附录A中表A-7的目标9一致)，需要验证额外代码，用验证结果E1论证该目标是否实现.论证2结构依据S1进行分解论证，G3说明结构覆盖率达到了规定的要求，也要用验证结果E1论证该目标是否实现.论证3结构依据S2进行分解论证，G4说明所有的问题都被记录并解决，并依据问题的不同，提出需要满足的不同的要求G5，G6，G7，G8(如图7所示)，并在对应的上下文描述中说明其约束条件，其中G8依据不同的停用代码使用情况，分解成目标G9，G10，并在目标G9,G10的上下文描述中说明其约束条件.最终用问题报告E2论证该目标是否实现.其中对证据E1，E2的结构要求定义在其对应的上下文中.

3.3.3 应用方法

实例化的步骤与3.1.3节应用方法中的1，2，3，4，5一致.如果在结构测试覆盖率分析过程中没有发现错误，那么G4中的变量P使用null表示，由于G4是DO-178C中规定必须执行的活动，因此G4不能删除.

需要特别指出的是，如果规定的项目不是A级软件，应删除子目标G2，否则不删除.

以操作系统S为例，采用上述方法实例化论证模式，最终建立了其针对DO-178C附录A中表A-7的目标7的论证结构，如图8所示:

Fig. 8 An example of test coverage of structure argument structure图8 结构测试覆盖率论证结构示例

图8中，先对G1进行实例化，说明论证的总目标是A级软件S的语句覆盖率符合标准.依据模式中定义的策略S1，S2和目标G2，将总目标G1向下分解.

1) 实例化目标G2的论证结构.描述A级软件必须对额外代码进行验证，通过证据E1证明是否符合这项目标.

2) 实例化策略S1的论证结构.在本例中，计算软件的语句覆盖率，依据实际情况，需要论证源代码语句覆盖率(目标G3)，并通过证据E1来证明是否符合这项目标.

3) 实例化策略S2的论证结构.在本例中，由于在结构覆盖率分析过程中发现存在停用代码的问题，因此需将图6中的G4实例化为图8中的G3.1，在进一步向下分解时，删除图7模式中其他不符合的目标G5，G6和G7.停用代码F1由于已经被其他代码取代因而不会再被调用，因此图8中G5.1对应于图7中的G9，并将图7中G9的约束条件以假设的形式添加到图8中的目标G5.1中，即保证该代码在任何情况下都不能被调用.并通过证据E2证明是否符合这项目标.

3.3.4 产生效果

建立结构测试覆盖率论证模式，有助于对不同项目实现DO-178C附录A中表A-7的目标5～7的论证结构提供便利.论证模式包含了DO-178C针对这些目标规定的所有需要执行的活动，即在该模式中标注了标准中规定的所有相关活动，并且列举出了不同等级软件需要实现的不同目标，因此最终建立的论证模型符合标准规定，并可通过规范的步骤实例化.在实例化的过程中，对于前2个论证结构(图6中的G2和S1)，不同的项目之间区别不大，但是对最后一个论证结构(图6中的S2)，则需依据项目的实际情况进行实例化，不同的项目之间存在差别.

3.4 论证模式关联

本文提出了上述3种针对DO-178C软件测试过程目标的论证模式.依据DO-178C中对软件测试活动的定义，软件测试活动分为执行不同类型的测试、进行需求测试覆盖率分析和进行结构测试覆盖率分析这3种，主要实现的目标是DO-178C中附录A中表A-6以及表A-7中包含的目标.本文提出的3种模式可以实现DO-178C规定的软件测试过程中的9个目标.同时，这3种模式在软件测试过程目标的论证中缺一不可、相辅相成.

4 方法对比分析

4.1 描述内容对比

以3.1.3节提到的机载操作系统A为例，本节分别使用本文提出的目标符合性论证模式以及GQM方法进行论证，建立论证结构，并对论证效果进行对比.

图9所示为论证操作系统A是否满足DO-178C附录A中表A-7的目标7的GQM论证结构.对其中的每个问题，都对应着1个度量来回答该问题.

通过图9建立的模型，论证人员可以找到度量中提到的数据来评估该操作系统是否满足目标.

基于本文提出的目标符合性论证模式建立的DO-178C附录A中表A-7的目标7的论证结构如图8所示.将这2种方法进行对比，可以发现图9建立的模型相对简单，因此只能粗略地列举需要论证的目标和所需的度量，难以根据需要逐层细化复杂论证结构，比如在图9中：

1) 论证的过程只能分为3层，因此描述的论证结构过于简单，难以进一步细化复杂的论证问题.例如问题3：是否所有存在问题都已经解决，没有明确说明对于不同类型的问题，什么样的处理方式才是合适的.

2) 针对论证目标，对应的度量数据难以进一步细化定义，因此可能存在歧义.对数据的理解不同会直接影响论证的结果.例如，需要语句覆盖率的运算结果，但是没有说明语句覆盖率的来源及其必需包含的内容.

GoalPurposeIssueObject(Process)ViewpointAchieveStatementcoverageSoftwareverificationprocessFromthecertificationauthoritiesQuestion1Whatisthecurrentstatementcoverage？Metrics1Statementcoverage=Testedstatement∕AllstatementQuestion2Isthestatementcoverageachieved？Metrics2StatementcoverageSubjectiveevaluationofcertificationauthori⁃tiesQuestion3Allproblemsaresolvedornot？Metrics3Problemreports

Fig. 9 The GQM model of objective 7 in table A-7
图9 表A-7目标7的GQM论证结构

对于图9中存在的上述问题，在图8建立的论证结构中都得到了解决.依据本文提出的方法建立论证结构，对论证目标及其上下文的约束和证据及其数据结构约束等都有更加完整明确的规定和清晰的表达方式.

4.2 成本对比

此外，本文提出的基于模式的目标符合性论证方法可以显著提高论证结构的可重用性，有效地降低面向标准的目标论证结构的建立成本，即工作量.假设建立1个论证结构的成本为1.由于建立1个GSN论证结构与建立1种相应的论证模式的成本是大体相当的，亦可视为1，因为其主要工作量主要是对标准的理解和论证要素的提取.由于实例化论证模式相对简单，绝大多数步骤仅仅是对模式变量值的选择等，因此其成本可以忽略不计.

以另一个机载嵌入式实时操作系统B为例，表1展示了直接使用GSN建立论证结构，以及使用本文提出的模式建立论证结构来论证DO-178C软件测试过程目标的成本.

Table 1 The Cost of Constructing Argument Structure

在操作系统B中，高层需求共有708项，低层需求共有3 207项.依据高层需求，整个系统分为4个子系统.依据低层需求，整个系统分为52个模块.在建立DO-178C附录A中表A-6的目标1～2的论证结构时，需要为每个子系统的每种特征(包含时间相关需求的子集、包含状态转换需求的子集、包含其他需求的子集)分别建立论证结构，用以分别判断其对应的测试用例是否符合DO-178C标准中规定的测试用例设计准则，因此，需要为每个目标分别建立12个论证结构.同理，在建立DO-178C附录A中表A-6的目标3～4的论证结构时，针对52个模块，需要为每个目标分别建立156个论证结构.因此，对论证DO-178C附录A中表A-6的目标1～2，直接建立GSN论证结构的成本均为12.对论证DO-178C附录A中表A-6的目标3～4，直接建立GSN论证结构的成本均为156.然而，建立上述4个目标的论证结构，如采用本文提出的第1种论证模式，通过实例化来建立上述论证结构，则其成本则近似为1.

同样，由于有4个子系统，所以，针对论证目标DO-178C附录A中表A-7的目标3～4 和DO-178C附录A中表A-7的目标5～7，直接建立GSN论证结构的成本均为4，合计20.而采用本文提出的方法，则仅需要分别实例化第2种和第3种论证模式，因此，基于模式建立论证结构的成本均为1，合计为2.

通过本案例可以看出，本文提出的模式能够应用于目标论证结构的建立和实例化工作中，并且能够有效的降低建立论证结构的成本，提高了效率.

5 结束语

本文提出一种基于论证模式的标准符合性论证方法，并重点针对DO-178C对软件测试过程提出的主要目标和要求，提出了3种对应的目标符合性论证模式，以及基于这些模式建立面向特定软件项目的目标符合性论证结构的实例化方法.本文提出的3种论证模式覆盖了软件测试过程涉及到的主要目标.在第4节中，以1个机载操作系统软件项目为案例，说明了利用本文提出的模式建立论证结构的有效性.接下来，我们的工作重点是如何将这种基于论证模式的目标符合性论证方法进一步应用于DO-178C的其他过程目标论证以及其他安全性标准的目标论证工作中.

[1]RTCA. DO-178C software considerations in airborne systems and equipment certification[S]. Washington: RTCA Inc, 2011

[2]Kelly T, McDermid J. Safety case patterns—Reusing successful arguments[C]Proc of IEE Colloquium on Understanding Patterns & Their Application to Systems Engineering. London: IET, 1998

[3]Holloway C M. Explicate’78: Discovering the implicit assurance case in DO-178C[C]Proc of the 23rd Safety-Critical Systems Symp. North Charleston, South Carolina, USA: CreateSpace Independent Publishing Platform, 2015: 205-225

[4]Holloway C M. Towards understanding the DO-178CED-12C assurance case[C]Proc of the 7th IET Int Conf on System Safety, Incorporating the Cyber Security Conf. London: IET, 2012: 1-6

[5]Spriggs J. GSN—The Goal Structuring Notation: A Structured Approach to Presenting Arguments[M]. Berlin: Springer, 2012

[6]Hu Ning. Study on airworthiness concerns of changes of DO-178C[J]. Aeronautical Computing Technique, 2014, 44(4): 94-98 (in Chinese)(胡宁. 从DO-178C的新变化透视软件适航关注点[J]. 航空计算技术, 2014, 44(4): 94-98)

[7]Zhang Juncai, Wang Juan, Pan Wei, et al. Research on structural coverage analysis based on DO-178B[J]. Aeronautical Computing Technique, 2011, 41(4): 67-69 (in Chinese)(张军才, 王娟, 潘卫, 等. 基于DO-178B的结构覆盖分析研究[J]. 航空计算技术, 2011, 41(4): 67-69)

[8]Federal Aviation Administration (FAA). Order 8110.49 Software Approval Guidelines[S]. Washington: Federal Aviation Administration (FAA), 2003

[9]Basili V R, Caldiera G, Rombach H D. The goal question metric approach[J]. Encyclopedia of Software Engineering, 1994, 2: 528-532

[10]Object Management Group (OMG). Kernel and Language for Software Engineering Methods (Essence), Version 1.1[S]. Needham, MA: Object Management Group (OMG), 2015

[11]Goal Structuring Notation Working Group. GSN Community Standard, Version 1[S]. York: Origin Consulting (York) Limited, 2011

[12]Takai T, Kido H. A supplemental notation of GSN aiming for dealing with changes of assurance cases[C]Proc of 2014 IEEE Int Symp on Software Reliability Engineering Workshops. Piscataway, NJ: IEEE, 2014: 461-466

[13]Matsuno Y, Taguchi K. Parameterised argument structure for GSN patterns[C]Proc of the 11th Int Conf on Quality Software. Piscataway, NJ: IEEE, 2011: 96-101

[14]Alexander R, Kelly T, Kurd Z, et al. Safety cases for advanced control software: Safety case patterns, FA8655-07-1-3025[R]. York: Department of Computer Science, University of York, 2007

[15]quainzk. The implementation of lock in operating system[EBOL]. [2016-05-08]. http:blog.sina.com.cnsblog_75f0b54d0100r7af.html (in Chinese)(quainzk. 操作系统中锁的实现原理[EBOL]. [2016-05-08]. http:blog.sina.com.cnsblog_75f0b54d0100r7af.html)

Yang Yang, born in 1991. Master. Her main research interests include safety certification and software engineering.

Wu Ji, born in 1974. Associate professor and PhD in Beihang University. Member of CCF. His main research interests include software safety, software engineering, software testing and requirement engineering.

Yuan Chunchun, born in 1985. PhD candidate in Beihang University. His main research interests include software engineering, software safety and software reliability (yccnankai@buaa.edu.cn).

Liu Chao, born in 1958. Professor and PhD supervisor in Beihang University. Senior member of CCF. His main research interests include software engineering, software safety and software testing (liuchao@buaa.edu.cn).

Yang Haiyan, born in 1974. Master and lecturer in Beihang University. Her main research interests include software engineering, software testing, software safety and requirement engineering (yhy@buaa.edu.cn).

Xing Liang, born in 1983. Engineer in Xi’an Aeronautics Computing Technique Research Institute, Aviation Industry Corporation of China. His main research interests include safety certification and software engineering (lionxing@163.com).

Objectives Conformity Argument Patterns for Software Testing Process in DO-178C

Yang Yang1, Wu Ji1, Yuan Chunchun1, Liu Chao1, Yang Haiyan1, and Xing Liang2

1(SchoolofComputerScienceandEngineering,BeihangUniversity,Beijing100191)2(Xi’anAeronauticsComputingTechniqueResearchInstitute,AviationIndustryCorporationofChina,Xi’an710068)

Safety-critical software has been widely used in many fields. As the specific requirement of safety-critical software is preventing catastrophes, this kind of software must comply with its relevant safety standards. But now it does not have any effective ways to construct objectives conformity argument model for standards. By analyzing the features of objectives of software testing process in DO-178C, an objective conformity argument pattern description framework based on GSN is proposed, and these patterns are described through four fields: the problems that we need to solve, the specification for the solution, the approach to use them and the effect after using them. At the same time, some extensions for safety case patterns are proposed to describe the objectives conformity argument patterns. On this basis, three objectives conformity argument patterns based on software testing process in DO-178C are proposed, which are code-requirement conformity argument pattern, test coverage of requirements argument pattern and test coverage of structure argument pattern. At the same time, the instantiated method to build the objectives conformity argument structure for a specific program based on these patterns is proposed. People can construct objectives conformity argument structure for objectives of software testing process in DO-178C effectively through the proposed way. At last, one case study, which is an embedded real-time operating system, indicates that the objectives conformity argument patterns proposed here are useful and effective.

safety-critical software; airworthiness certification; DO-178C; GSN; argument patterns

2015-12-09；

2016-11-04

吴际(wuji@buaa.edu.cn)

TP311