航空电子认证中的正式程序验证

在正式采用新的DO-178C / ED-12C标准及其补充（包括关于形式方法的DO-333 / ED-216补充）五年后，尚未有航空电子认证项目承认使用这一新补充。然而，确实存在形式化的方法技术，可以简化航空电子软件的开发。

阻碍采用正式程序验证进行航空电子认证的主要障碍是，尽管开发DO-333 / ED-216的委员会进行了大量的传播工作，但缺乏关于如何应用DO-333 / ED-216的普遍共识。现在有一个详细的过程，用于使用 SPARK 来满足 DO-333/ED-216 的目标，作为某些形式的测试的替代品，重点是检查源代码是否一致、准确并符合低级要求。

该过程解决了使用正式方法时的替代覆盖目标以及源代码和可执行目标代码之间的财产保护目标。当某些测试被使用正式方法所取代时，前者是必需的。后者是必需的，以便从可执行目标代码的源代码验证中受益。已与美国联邦航空管理局（FAA）和欧洲航空安全局（EASA）讨论了此过程，以便将来在DO-178C / ED-12C中使用SPARK的申请人。

航空电子学中的形式化方法

尽管在DO-178的C版中添加正式方法补充是2012年，但使用正式方法开发航空电子软件至少可以追溯到1990年代，当时John Rushby写了一份关于它们用于FAA的全面指导文件。［“形式方法和关键系统的认证”，拉什比，FAA，1993年。虽然Rushby专注于演绎方法，但从那时起自动化和计算机能力的提高使得另外两种形式化方法对开发航空电子软件具有吸引力：模型检查和抽象解释。DO-333专门针对使用这三类形式化方法来开发航空电子软件。美国宇航局2014年的一份报告中介绍了所有三个类别的使用示例［“DO-333认证案例研究”，Cofer和Miller，Rockwell Collins，2014年。

图1：DO-333 验证活动。图形由IEEE提供。

虽然抽象解释和模型检查非常适合以最少的人为干预检查代码库中的简单程序属性，但它们会遇到所谓的状态爆炸问题，当分析的模型的大小（无论是在模型检查中显式提供还是由工具从抽象解释构建）太大而无法完成分析时。演绎方法没有这些缺点，但它们有要求用户编写函数合约的成本。这些协定是函数行为的（部分）规范，既定义了验证目标，也定义了用于分析对该函数的调用的函数行为的适当摘要。这允许演绎方法应用强大的验证技术，这些技术可以证明软件的非平凡属性，因为函数合约使焦点能够专注于对单个函数的验证，一次一个。

两个工具集为C和Ada的工业用户提供基于演绎方法的形式程序验证：用于C程序的Frama-C工具集和用于Ada程序的SPARK工具集。两者都被用于DO-178航空电子设备认证。例如，洛克希德马丁公司最初在1997年将SPARK用于C-130J美国军方和英国皇家空军飞机的控制软件。此后，BAE系统公司使用SPARK在维护期间证明了C-130J控制软件的关键特性。另一个例子，在DO-333中记录，空中客车公司在2002年使用Caveat（Frama-C的前身）来证明对空中客车A380民用飞机的低级要求，作为单元测试的替代品。

B. 所处理的核查目标

SPARK 可用作 DO-333 中许多验证目标的主要证据来源，从低级要求 （LLR） 到源代码和可执行目标代码 （EOC）。形式验证是分析的一个特殊情况，因此将形式分析应用于LLR和源代码所需的指导只是使用形式分析的标准和条件。［“在认证环境中使用形式方法的指南”，Brown 等人，SC-205/WG-71，ERTS 2010。在EOC中使用需要更多的理由，特别是在替换单元测试时。

当 LLR 在 SPARK 中表示为合约时，正式符号保证 LLR 是精确和明确的，因此准确性是有保证的。一致性也得到了保证，因为不同功能的合同不会冲突。合约也是可验证的，并且通过设计符合（编程语言）标准。这些包括表FM的目标2、4和5。来自DO-4的A-333。（同前科弗和米勒。

SPARK 的主要资源之一是它自动显示源代码符合以函数契约表示的 LLR。函数协定还可以表达数据依赖关系，SPARK 工具集可以自动显示源代码符合软件体系结构的这一部分。SPARK代码是可验证的，并且符合（编程语言）标准的设计。函数的源代码隐式追溯到函数协定中表示的 LLR。最后，SPARK 代码是明确的，因此可以自动分析源代码的一致性，以表明它没有未初始化数据的读取、算术溢出、其他运行时错误和未使用的计算（变量、语句等）。这些指标包括表FM的目标1至6。来自DO-5的A-333。

平机会在LLR方面的合规性和稳健性的目标（表FM的目标3和4。DO-333的A-6）可以通过依赖源代码的相应目标来解决，前提是同时提供源代码和EOC之间的财产保护演示。显示财产保全的一种方法是合理地证明，在所有可能的情况下，编译器都保留了从源代码到EOC的程序语义。不幸的是，似乎没有任何合理的办法能够提供这种信心。通过在SPARK中执行合约的模式下运行集成测试，用户可以确信编译器在EOC中正确保留了源代码的语义;否则，在单个函数中证明的合同将在集成测试中（很有可能）失败。通过在执行和不执行合约的情况下运行集成测试并检查输出是否相同，用户可以确信合约的编译不会影响代码的编译，因为否则在某些测试中输出很可能会有所不同。

当然，使用 SPARK 的一个主要好处是能够通过 SPARK 分析替换单元测试。在这种情况下，DO-333还定义了表FM的附加目标5至8。A-7.正式验证和审查的结合可以实现这些目标，正如空中客车和达索航空过去的经验所证明的那样。［“测试或形式验证：DO-178C 替代方案和工业”，Moy 等人，IEEE Software 2013。这里使用了 SPARK 的几个功能，例如在函数契约中声明数据依赖关系的能力，以及通过不相交的情况表达函数契约的可能性。

即将上来

自 1990 年代以来，一些先驱者一直在使用正式的程序验证工具集。航空电子软件认证中正式程序验证自动化的进展现在使更多公司可以使用这些技术。SPARK使用户能够解决DO-178C的形式方法补充DO-333中定义的许多验证目标。美国和欧洲的认证机构现在正在看好在航空电子认证中使用这种方法的申请人。

审核编辑：郭婷