一、引言

在现代航空工业中，软件已成为飞行控制、导航、通信及机载娱乐等系统的核心组成部分。随着航空器系统复杂度的不断提升，软件的安全性、可靠性和确定性变得至关重要。DO-178C为不同安全关键等级的软件规定了全生命周期内应遵循的目标、活动和流程，成功支撑了无数安全关键航空软件的开发与审定，为全球航空安全做出了卓越贡献。然而，传统基于测试的验证方法在面对日益复杂、高集成的系统时，面临验证覆盖度难以完备、错误发现滞后、成本高昂等挑战。DO-333在此背景下应运而生，为形式化验证技术融入航空软件认证工程提供了官方指南和合规路径，共同开启了一个高可靠认证的新范式。

二、DO-333加持 DO-178C：航空软件高可靠认证新范式

DO-333并非直接取代DO-178C，而是作为其补充指南，专门阐述如何应用形式化方法来满足DO-178C中更高的安全目标，解决了多种传统验证方式难以解决的问题：

• 提升验证的严谨性与完备性：传统测试本质上是抽样验证，无法穷尽所有可能状态。形式化方法通过数学建模和逻辑推理，可以对系统行为进行穷尽性分析，证明关键属性在所有可能情况下均成立，或精准定位违反属性的反例。这显著增强了验证的可信度。

• 实现缺陷的早期预防与发现：形式化方法可在需求与设计阶段早期应用。通过形式化建模和分析，能够发现需求中的模糊、矛盾、不可实现或潜在危险状态，将缺陷扼杀在萌芽阶段，大幅降低后期修改的昂贵成本。

• 应对复杂系统与高安全性要求：对于涉及复杂并发、状态机交互或高安全等级（DAL A/B）的系统，传统方法难以保证充分覆盖。形式化方法擅长处理此类复杂度，为最关键的软件部分提供更高层级的保证。

• 优化验证证据的生成：DO-333明确了形式化方法可以替代或补充DO-178C中特定的验证目标（尤其是高层需求验证、设计与需求一致性验证等）。形式化工具生成的证明或分析报告，可作为强有力的客观证据，支撑符合性论证，使评审过程更具条理性和说服力

值得注意的是，DO-333主要并强烈推荐用于DAL A和B级软件的开发与验证。对于DAL C级，可以有选择性地应用。对于DAL D/E级，则通常没有必要。

三、未来趋势：DO-178C持续赋能航空领域

DO-178C作为基石标准，其地位在未来相当长一段时间内仍将稳固。然而，其内涵与实践方式正在与以DO-333为代表的新技术深度融合，共同演进，DO-178C与DO-333共同作用的框架面向多个不同领域提供了适应性。随着航空软件更新频率加快，需要更敏捷、更可靠的验证手段，对于高完整性软件（DO-178C Level A/B），形式化验证可以直接替代“结构覆盖率测试”，显著降低人力和时间成本。形式化验证正能快速响应用例变更和需求迭代，为持续验证和持续适航提供技术支撑。浙江望安科技有限公司面向需要通过DO-178C认证的企业提供形式化验证，可帮助企业设计可适配多重要求的密码模块架构，制定高效的跨区域认证策略，破解信任根互认难题，为企业产品全球化布局提供一站式的解决方案。