航空航天领域-FGS单侧模式逻辑形式化验证

案例描述

本案例来源于《Formal methods case studies for DO-333》，展示了形式化方法在航空航天飞行控制软件中的应用。针对飞行导引系统（FGS）单侧模式逻辑进行形式化验证，确保其满足规约要求和飞行控制法则。模式逻辑是飞控系统的核心组成部分，直接影响飞机的导航和自动驾驶行为，其正确性对飞行安全至关重要。FGS模式逻辑虽然复杂，但输入输出均为布尔值，非常适合使用模型检查进行形式化验证。

案例实施的具体内容

• 模式逻辑建模：将FGS模式逻辑分为三类：非布防模式（Non-Arming Mode）、布防模式（Arming Mode）、捕获/跟踪模式（Capture/Track Mode），对每种模式的状态及状态转换进行精确定义。
• 模型转换：将FGS模式逻辑描述转换为模型检查器可接受的规范语言（如Lustre形式）。
• 规约和性质规范编写：根据DO-178C和DO-333标准，定义软件设计验证目标，包括高层与低层软件需求的一致性。
• 模型检查：使用隐式状态BDD模型检查器（NuSMV）和SMT模型检查（Kind）进行验证，检测潜在错误与反例。
• 错误修正与重复验证：发现16个错误后，开发团队进行修正，并重新验证直到所有目标满足。

案例亮点

• 精确规约：将复杂模式逻辑用形式化语言精确定义，避免模糊解释。
• 全流程验证：涵盖高层软件需求、低层软件需求和架构一致性验证。
• 自动化验证与错误发现：利用模型检查器自动检测潜在错误，发现16个隐藏错误，包括命名错误导致的逻辑问题。

实践效果

• 提升软件可靠性：通过形式化验证，确保FGS模式逻辑完全符合设计规约，提高飞控系统的安全性。
• 降低后期成本：在开发早期发现错误，减少后期修复代价和返工风险。

应用价值

该案例为飞行器自动导航和自动驾驶功能提供可靠的软件保障，逐步推动形式化方法在航空航天领域的标准化应用和评审流程采纳。