DO-332帮助解决OOT的动态灵活性关键认证挑战

DO-332是DO-178C标准对面向对象技术（OOT）和相关技术的补充，分析了安全关键软件中面向对象引发的问题，并为处理OOT的漏洞提供了新的指导。DO-332的一个重要新目标是“本地类型一致性验证”，它利用了称为“Liskov替换原理”的类型理论结果，并帮助解决OOT的动态灵活性带来的一些关键认证挑战。

面向对象技术（OOT）被广泛使用，并得到包括C++，Java和Ada在内的一系列编程语言的支持，但由于各种原因，它的普及尚未扩展到机载和其他安全关键软件。根本问题是验证利用OOT三个基本元素的软件的复杂性：继承，多态性和动态绑定。（图 1 说明了面向对象的基础知识。一个简单的例子说明了这些问题：

图1：面向对象基础知识

假设 Sensor 类是继承层次结构的根，ref 是对此层次结构中任何类中的对象的多态引用，而 Reset 是为不同的 Sensor 类定义不同的操作。声明参考。Reset（。..） 根据 ref 表示的对象的类动态绑定到相应的版本。如何验证此调用是否满足重置操作的要求？

如果使用继承来定义不是传感器专用化的子类，则会出现一个问题。此子类的重置可能具有与重置传感器无关的某些效果，或者可能会生成异常。ref 从这样的子类引用对象将是一个错误，需要分析以表明错误不会发生。这使验证过程复杂化。

另一个问题涉及结构覆盖率分析。对于 DO-178 标准中三个最高级别（A、B 或 C）中的任何一个的系统，必须使用基于需求的测试来证明完整的语句覆盖率。但是，编译器可能会选择几种实现策略来处理动态绑定，这些策略对“语句覆盖率”的含义有不同的含义。结构覆盖范围的范围不应取决于编译器使用的实现策略。

DO-332［1］是DO-178C［2］的OOT补充，通过局部类型一致性的新概念解决了这些问题，该概念利用了继承只应用于类专用化的原则。

继承和利斯科夫替代原则

在面向对象的设计中，系统的体系结构反映了类及其关系。一个特别重要的关系是专业化（“is a”），但还有很多其他关系。实现设计涉及选择用于捕获关系的语言机制。

在面向对象的语言中，继承可用于实现两个类之间的各种关系。但是，当继承用于专用化以外的任何内容时，可能会出现异常，因为为超类定义的操作可能对子类没有意义。在类型论的背景下，已经研究了将继承限制为专业化关系，其中它被称为Liskov替换原理（LSP）［3］。非正式地说，LSP 意味着无论在哪里可以使用超类的实例，都应该允许替换任何子类的实例。

使用继承进行专业化与操作的前置条件和后置条件（其“协定”）具有重要的交互作用。前提条件是在调用操作时对程序状态所做的假设。后置条件是保证操作在操作完成时对程序状态进行的操作。前置和后置条件可以明确指定 - 可以在源文本中指定，如Ada 2012［4］或SPARK［5］，也可以单独指定 - 或者它们可以隐含在操作逻辑中。

如果继承符合 LSP，则操作的子类版本不应施加比超类版本更强（更具限制性）的前提条件。否则，调用可能在某些情况下（在超类实例上）成功，但在其他情况下（在子类实例上）失败。类似地，子类的操作版本不应指定比超类版本更弱（更通用）的后置条件。

因此，符合 LSP 意味着满足两个属性：

协定一致性：任何子类操作都不会加强它所覆盖的超类操作的前置条件或削弱后置条件。

行为一致性：每个子类操作都满足其超类的要求。

DO-332 在新目标“本地类型一致性验证”中捕获了这些概念。此目标不需要证明类层次结构符合 LSP，这将过于严格。相反，它反映了对于符合要求的类体系结构，验证工作更简单，并且分析只需要考虑本地上下文。

本地类型一致性

图 2 显示了与验证本地类型一致性相关的活动，DO-332 需要 A、B 或 C 级别的软件。“对于使用替换的每个子类型”的措辞是指发生动态绑定的上下文，例如 ref。Reset（。..），所讨论的“子类型”是 ref 在这一点上可以引用的对象的类。潜在的类不一定是完整的层次结构，不同的类集可能适用于同一操作的不同调用。

图2：与验证本地类型一致性相关的活动，DO-332 要求级别为 A、B 或 C 级软件

考虑引用的特定出现。Reset（。..），并让 HeatSensor 成为 ref 可以在那里引用的对象可能的子类之一。引用的本地类型一致性。HeatSensor的重置（。..）可以“乐观地”或“悲观地”地证明。如果HeatSensor满足LSP，则乐观方法有效，可以通过两种方式进行：

通过形式化方法，通过证明HeatSensor的复位版本满足传感器版本的要求，并且不会加强传感器复位的前置条件或削弱后置条件。

通过测试，通过使用 HeatSensor 的实例对传感器的重置版本运行基于要求的测试。

来自编程语言及其工具集（例如 Ada 2012 或 SPARK）的适当支持可以促进形式化方法。

乐观的方法将证明超类和子类的操作版本之间的契约和行为一致性。通过对子类的基于需求的测试以及可能通过形式化方法获得额外的验证。

如果类不符合 LSP，或者动态绑定调用很少，或者层次结构很浅和/或很窄，那么测试可能出现的每种可能的情况可能是最简单的。这是图 2 中第三个项目符号项中指定的悲观测试。需要基于需求的测试来对可能出现的每个子类执行操作。

DO-332、本地类型一致性和 LSP 指南认证

本地类型一致性验证只是安全使用 OOT 的一个方面;DO-332 包含有关其他 OOT 元素以及相关技术（如通用模板）的指南。DO-332 是“语言不可知论者”;有关如何使用 Ada 2012 作为编程语言在安全关键或高安全性系统中应用 OOT 的更多细节［6］。

DO-332 的本地类型一致性指南与 DO-178C 的一般验证方法一致，确保所有测试都基于要求。它以一种新颖的方式调整验证活动，以反映面向对象的语义和类结构对LSP的遵守程度。新指南应有助于促进面向对象编程（OOP）在航空电子设备和其他关键领域的安全使用。

审核编辑：郭婷