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

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

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

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

传统的测试方法

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

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

从高级需求中导出模块级需求，这些需求足够具体以确定适当的实现

使用单元测试检查实现的每个模块是否符合其低级需求

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

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

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

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

【图1 | 由于易于使用，集成测试优于单元测试。］

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

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

集成单元测试

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

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

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

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

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

受信任的代码生成器

如果我们要越来越依赖此类工具来帮助从更高级别的模型自动生成安全关键软件，那么建立对代码生成器的信任至关重要。但是，需要创新方法来管理以最高信任级别 TQL-1 实现现代优化代码生成器的工具认证的潜在高昂费用。集成单元测试就是这样一种方法。当与其他正式指定需求的系统方法相结合，并根据这些需求生成需求监控器和预言机等组件时，就有可能以一种不仅更具成本效益，而且支持增量认证的方式实现 TQL-1。工具进化。AdaCore 正在使用这些方法验证其 QGen 代码生成器。

审核编辑：郭婷