在基于模型的自动代码生成器中建立信任

星星科技指导员 2022-11-11 563

描述

您如何建立对用于安全关键系统的自动代码生成器的信任？例如，给定一个代码生成器，它采用 Simulink 和 Stateflow 中表示的飞行控制系统的实时模型，并将其转换为 MISRA C 或 Ada 的 SPARK 子集，哪个过程可以确保生成的代码是原始实时模型的忠实表示？美国联邦航空管理局（FAA）有一个定义明确的流程来创建合格的代码生成器，这意味着一个代码生成器，其输出可以信任为与输入模型的语义完全匹配，没有遗漏任何内容，也没有添加任何内容。此过程在 DO-178C（机载系统中的软件注意事项）及其随附的文档 DO-330（软件工具认证注意事项）和 DO-331（基于模型的开发和验证）中定义。

对于像代码生成器这样的工具，可能会将错误插入机载系统，如果要将工具用于故障可能是灾难性的子系统（A 级子系统），则需要最高级别的工具资格（工具资格级别 1 （TQL-1））。

毫不奇怪，这种级别的工具鉴定可能涉及大量的时间和精力，通常估计为每 1，000 行代码（KSLOC）数百小时。这类似于验证 A 级安全关键型嵌入式软件组件所需的每行工作量。但是工具可以有更多的代码行。例如，如果该工具是100 KSLOC，则传统的A级验证方法可能花费约500万美元。因此，有强烈的动机研究测试此类工具的替代方法，同时仍然实现TQL-1目标。

传统的测试方法

验证高完整性应用程序的传统方法要求测试人员：

仔细定义和验证应用程序的一组高级要求

从高级需求派生模块级需求，这些要求足够具体，可以确定适当的实现

使用单元测试根据其低级需求检查实现的每个模块

对所有高级需求执行集成级测试

然后执行覆盖率分析，以确保这些测试涵盖所有代码，并确保应用程序中没有可能提供额外、不需要的功能的代码。

对于嵌入式软件组件，每个模块的单元级测试和整个组件的集成级测试的组合可以很好地工作。特别是，嵌入式软件模块的单元测试是实用的，因为在许多情况下，每个模块的输入数量和复杂性是可管理的，并且输出相对容易识别和检查。但是，对于像自动代码生成器这样的工具，它通常涉及多个阶段，涉及将输入模型逐步转换为生成的代码，单元测试可能是一个真正的挑战。另一方面，对于这样的工具来说，集成测试并没有明显困难，因为中间阶段的数量不会影响工具的整体输入和输出。

图 1 说明了单元测试的复杂性与多阶段工具（如代码生成器）的集成测试相对容易程度之间的这种二分法。

嵌入式

［图1 |由于易于使用，集成测试比单元测试更受欢迎。

在图 1 中，我们显示了优化自动代码生成器的整体数据流，其中输入模型称为“用户语言”，输出称为“源代码”。多个阶段被流水线化，原始模型中的第一阶段读数以用户语言（M0）表示，并以某些内部数据结构（M1）表示模型。然后将其转换为模型的较低级别表示（M2，M3等），直到最后阶段以所需的编程语言生成实际的源代码。要执行集成测试，只需使用常规模型创建工具准备一个以用户语言表示的模型，将其馈送到代码生成器中，然后检查生成的源代码，以确定它是否满足形式和功能方面的高级要求，使用普通编译器、静态分析和该编程语言的测试工具。

相比之下，对多相代码生成器的每个阶段执行单元测试要复杂得多。必须为给定阶段的每个测试构建一个内部数据结构，该结构符合用于该阶段输入的表示形式，然后需要对该输入调用该阶段，然后必须检查输出表示以查看它是否具有预期的形式和内容。准备此类输入并检查此类输出需要费力的手动过程或创建特殊工具，这些工具本身可能需要认证。

集成单元测试

鉴于单元测试的复杂性，已经开发了一种称为集成单元测试的替代方法。图 2 说明了此方法：

嵌入式

［图2 |集成单元测试方法是单元测试的更简单替代方法］

在图 2 中，我们展示了一个将单元测试需求监视器和单元测试预言机（一个“知道”所需输出的检查器）直接嵌入到工具结构中的过程。将这些监视器和检查器嵌入到工具中后，我们按照用于正常集成测试的步骤进行操作，准备代表性模型（Test0 到 Test4），并通过代码生成器将它们馈送。但是现在，每个嵌入式单元测试需求监视器不只是等待工具生成最终输出，而是跟踪其关联阶段的输入是否与其关联的单元测试匹配，如果匹配，它会记录该事实，然后触发相应的基于单元测试预言机的检查器，该检查器验证阶段的输出是否对应于特定测试模式的输入的预期转换。

例如，假设我们在模型级别定义了增益块的特定转换，将其转换为代码级别的表达式，该表达式将信号变量的值乘以常量。每当增益块出现在其模型级输入表示中时，我们都会有一个单元测试要求监视器记录，当它出现时，触发基于 oracle 的检查器查看代码级输出表示，以确保它涉及将适当的信号变量乘以适当的常数。这是一个非常简单的检查，只要有足够的模型作为一个整体通过该工具，就可以预期覆盖此特定的单元测试模式。

通过该工具运行多个模型后，我们最终可以得到一个如图 2 所示的表。在左侧，我们有模型，Test0到Test4。在顶部，我们有针对工具每个不同阶段的测试需求和测试预言机对。例如，tr0，2 表示阶段 0 的测试要求 2，而 to2，1 表示阶段 2 的测试预言机 1。每次阶段的特定输入满足与某些测试需求相关的测试模式时，我们都会在输入模型行的需求列中看到 SAT。每次调用测试预言机时，我们都会在输入模型行的预言机列中看到 PASS 或 FAIL。如果我们最终得到一个空列，则从未遇到测试模式（未涵盖相应的低级要求）。如果我们最终在 test-oracle 列中出现 FAIL，这意味着我们有一个测试失败（相应的低级需求没有正确实现）。在图 2 所示的表中，我们看到 tr0，1 和 tr2，0 未被覆盖，而 to0，2 和 to2，1 出现故障。这样的表记录了一个完整的单元测试过程，同时避免了为每个测试模式准备特殊输入的费用。

值得信赖的代码生成器

如果我们要越来越多地依赖此类工具来帮助从更高级别的模型自动生成安全关键软件，那么建立对代码生成器的信任至关重要。但是，需要创新方法来管理在最高信任级别 TQL-1 下实现现代优化代码生成器的工具认证的潜在高昂费用。集成单元测试就是这样一种方法。当与其他用于正式指定需求并从这些需求生成需求监视器和预言机等组件的系统方法结合使用时，可以实现 TQL-1，这种方式不仅更具成本效益，而且随着工具的发展支持增量鉴定。AdaCore 正在使用这些方法验证其 QGen 代码生成器，从而为基于模型的开发社区提供一种新工具，该工具可以成为整体高完整性、软件密集型系统工程流程的可信部分。

审核编辑：郭婷

打开APP阅读更多精彩内容