作者 | 徐奕龙飞 上海控安可信软件创新研究院系统建模组

版块 | 鉴源论坛 · 观模

社群 | 添加微信号“TICPShanghai”加入“上海控安51fusa安全社区”

01

摘 要

本文主要探讨了形式化方法在航空领域中的工业应用。航空领域作为安全攸关领域，其机载系统软件的开发有着高度复杂和严格的安全标准要求，以确保其安全可靠性。但是由于机载系统软件功能的增加，软件系统规模增大，系统整体更为复杂，使得传统方法难以满足飞行控制系统的验证需求。为解决航空领域的痛点，形式化方法成为一种有效的解决方案。形式化方法是一种基于数学和形式逻辑的工程方法，可用于系统设计、验证和分析。形式化方法的应用有助于确保飞行安全性、提高飞机性能和优化飞行控制系统。

02

航空领域的应用背景

在航空领域，飞行控制系统软件是核心的组成部分，对整个航空器起着决定性的作用，其安全性和可靠性对航空器的正常运行有着至关重要的作用，一旦软件出现故障，其造成的损失将会十分巨大。然而由于现代飞行控制系统软件非常复杂，涉及到软件和硬件的协同交互，传统的测试方法不仅需要耗费大量的人力资源和时间成本，还难以做到覆盖所有可能的情况，从而彻底规避安全隐患。这就使得在系统软件开发的流程中存在着需求或系统设计出现问题的风险。历史上，由于此类问题而造成的重大损失的灾难事故触目惊心。2007年，美国空军战斗机F-22的飞控软件设计时未考虑时差因素, 在跨越国际日期变更线时飞行员变更系统时间致使飞控系统锁死；2018年和2019年两架飞机由于飞行控制软件中反失速系统机动特性增强系统(MCAS)的缺陷发生了坠机事故导致总共三百余人死亡。

图1 典型软件事故：F-22和波音737-MAX事件（图片源自新闻）

人类航空史上血泪的教训促成了适航审定标准的不断完善。为了更好地保障机载软件的安全性和正确性，航空领域提出了DO-333标准。DO-333标准由RTCA专委会（航空无线电技术委员会）和EUROCAE工作组（欧洲民用航空设备组织）撰写，并已于2011年12月13日由RTCA程序管理委员会（PMC）审定通过，名为"Formal Methods Supplement to DO-178C and DO-278A"。其中DO-178C是航空领域的飞行器软件开发标准，而DO-278A是相关地面系统软件的开发标准。而DO-333是对两者的补充说明，旨在引导航空软件开发团队在软件开发生命周期中应用形式化方法。DO-333中对原有DO-178C中给出的目标、活动、解释性文字以及软件生命周期过程数据进行某些改变与补充。这些更改和补充包括了若干用形式化语言描述的文档，以及建立在这些形式化文档基础之上的形式化验证佐证材料。为此，DO-333专门作出了针对性的增补和调整。DO-333适航标准中将软件开发过程定义为四个环节，分别是软件需求过程，软件设计过程，软件编码过程和软件继承过程。并对各个软件开发过程提出了验证目标，并解释了如何应用形式化方法于软件开发的四个环节之中，阐述了其优劣所在。该标准的提出说明了在安全攸关的航空领域，形式化方法在工程上提升机载软件安全可靠性的能力得到了一定的认可，从而也引发了如何将其更好地应用于机载软件的研发和认证过程之中的探讨。

03

形式化方法的解决方案

形式化方法是建立在严格的数学基础上的针对数字化系统进行规格说明撰写、软件开发、软件验证的技术。形式化的数学基础主要包括形式逻辑、离散数学和机器可识别语言。形式化方法主要研究理念是工程人员希望通过合理的理论和工程方法特别是数学分析手段对软件设计的健壮性和正确性进行严格的分析，找出人力审查难以发掘的软件缺陷，满足人们对高质量软件可信的期望。形式化方法的主要特点是明确、无二义性的描述软件系统的需求，通过软件的形式化表达为软件的一致性、准确性提供严格验证。

形式化方法通常包含两类关键技术，分别是形式化建模和形式化分析。其中两者各自具有多种类型的实现技术。在形式化建模中，可以通过多种方法生成一个由无歧义的数学语法和语义定义的形式化模型，譬如说有形式化的图形模型，这里图的各个组件和他们之间的连接都有着严格的数学定义的语法和语义，比如SCADE工具中的状态机就是典型的形式化图形建模的案例。还有使用形式化建模语言描述的模型，例如Z语言、B方法、BIP。形式化分析方法可以归为3类：1）演绎方法（deductive），如定理证明，2）模型检查，3）抽象解释。

1）演绎方法：涉及数学推理，即通过数学方法证明形式模型性质。性质的数学证明为软件性质的正确性提供了严格证据。数学证明通常借助自动或交互式的定理证明系统。在一些情况下，即使借助定理证明系统，构建数学证明也会很困难，甚至无法构建。不过，一旦证明能构建成功，自动检查证明的正确性将会变得很容易。

2）模型检查：探索形式模型所有可能行为，从而判定指定性质是否成立。当性质不成立，模型检查算法自动生成一个反例，以确定该性质在何处不成立以及不成立的原因。在一些情况下，模型检查工具可能无法判定给定的性质是否成立。

3）抽象解释：是一种构建程序语言语义的保守表示（conservative）的理论（保守表示以确保可靠性）。实践中，该技术针对无限状态系统设计基于程序语义的分析算法，能静态、自动及可靠地分析系统动态性质。借助相应的工具 ，抽象解释为具体的性质产生形式模型。该技术可以看作部分地执行计算机程序，在无需实际操作所有计算任务的同时，确定程序间的重要影响关系（如控制流结构，信息流，堆栈大小，时钟周期的数目等）。

04

应用案例

本应用案例来源于" Formal methods case studies for DO-333."， 该资料分享了形式化方法在航空航天领域中的案例研究。为了检查系统规约是否满足特定性质和要求，应用模型检查来验证飞行导引系统（FGS）单侧模式逻辑的正确性。模式逻辑是飞行控制系统中的关键组成部分，它决定了飞机的导航和自动驾驶行为，其正确性对于确保飞行安全至关重要。在FGS中，模式逻辑相对复杂，但输入和输出仅有布尔值组成，这使得它适合使用模型检查进行形式化验证。

4.1 模式逻辑概述

模式指的是系统行为的互斥集合，对于FGS系统而言，模式对应于单个（或一组）FGS行为的系统配置，更贴切地说，FGS的模式就是其飞行控制法则的抽象，其模式逻辑主要包括三种不同类型的模式。

1. 非布防模式(Non-Arming Mode)：该模式只有CLEARED和SELECTED两个实际状态。如果由飞行机组手动请求或由FMS等子系统自动请求，模式被认为是SELECTED状态，否则被认为是CLEARED状态。

图2  Non-Arming Mode

2. 布防模式（Arming Mode）：该模式有三个状态：ARMED、ACTIVE和SELECTED。ARMED和ACTIVE是SELECTED状态的子状态，即当模式处于ARMED或ACTIVE状态时，它同时也处于SELECTED状态。

图3  Arming Mode

3. 捕获/跟踪模式（Capture/Track Mode）：该模式相比前一模式在ACTIVE中区分了捕获和跟踪状态。CAPTURE和TRACK状态都是ACTIVE状态的子状态，并且模式的飞行控制法则在这两种状态下都处于ACTIVE状态，即为飞行导引和自动驾驶系统生成指令。

图4  Capture/Track Mode

4.2 模型检查案例目标

本案例的目标是对FGS单侧的模式逻辑进行形式化验证，以确保它满足规约中的要求和飞行控制法则。使用模型检查来执行与软件设计过程的输出相关的验证活动，重点关注 DO-178C 中表 A-4 和 DO-333 中表 FM.A-4 的目标。这些验证活动的目的是检测软件设计过程中可能引入的任何错误（DO-178C 第 5.2 节）。具体来说，本案例将验证FGS一侧模式逻辑的低层软件需求，并表明软件架构和低层软件需求符合高层软件需求。其详细验证目标如表1所示。

表1 软件验证目标

4.3 模型检查工具和方法

在本案例中，使用了两种主要的模型检查器：隐式状态BDD模型检查器（如NuSMV）和SMT模型检查器（如Kind）。这两种模型检查器分别适用于不同类型的规约和验证需求。

验证流程：

1. 首先，将FGS的模式逻辑描述转化为模型检查器可接受的形式，例如Lustre形式的规范语言。

2. 确定并规定模式逻辑的各种状态和状态转换。

3. 编写规约和性质规范，涵盖所有目标验证要求。

4. 使用模型检查器对规约和性质进行验证，以查找可能的错误和反例。

验证结果：

通过模型检查器的验证，得到模式逻辑是否满足规约和飞行控制法则的结果。如果模型检查器找到了错误或反例，开发团队可以进行修正，重新验证，直到所有目标都得到满足。最终使用Kind模型检查器验证FGS模型的模态逻辑时，发现了共十六个错误。

模型检查发现的错误示例：

下面我们详细阐述如何使用模型检查工具发现错误的过程，图5是一个非常简单但是常见的命名错误，在退出ACTIVE模式时，输出变量LGA_Active（正确情况应该是VGA_Active）被设置为false。通过Kind模型检查器检测到了这个错误。Kind模型检查器产生的反例如图6所示。

图5  模型检查得到的错误示例

图6  模型检查得到的反例

该反例共有3个步长，显示了每一步的相关输入和输出的值。未发生变化的值用灰色文本显示。灰色背景标出了最重要的值，以帮助读者理解反例。在初始步骤中，ROLL_Active模式如预期一样处于活动状态。在第二步中，按下GA开关，激活了LGA模式。这同时激活了VGA模式。在第三步中，VS_Pitch_Wheel_Rotated激活，清除VGA模式，即从ACTIVE转变为CLEARED状态，但是，实际上在第三步中并没有清除LGA模式，但由于命名错误，输出变量LGA_Active却被错误地设置为false。

综上，形式化方法在航空领域已经开始受到越来越多的重视，并逐渐进入相关评审流程中。通过工业界实际的应用，形式化方法展现出了其在提高机载软件系统安全性和可靠性方面的价值。通过形式化方法，我们可以在软件开发生命周期的不同阶段，精确地定义系统规范和性质，并自动化地验证系统的正确性。形式化方法的发展将持续推动航空领域软件开发的创新和进步，为飞行安全提供更加可靠的保障。通过不断深入研究和实践，形式化方法将在航空领域继续发挥重要作用，为飞行控制系统的安全性和可靠性提供持续支持。未来，我们将继续介绍更多形式化方法的技术细节和更多的应用案例。

主要参考文献：

1. RTCA DO-333, Formal Methods Supplement to DO-178C and DO-278A (December 2011)

2. Cofer D, Miller S P. Formal methods case studies for DO-333[R]. 2014.

3. Platzer A, Quesel J D. European Train Control System: A case study in formal verification[C]//International Conference on Formal Engineering Methods. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009: 246-265.

4. Clarke E M. Model checking[C]//Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18–20, 1997 Proceedings 17. Springer Berlin Heidelberg, 1997: 54-56.

5. Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[C]//Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 1977: 238-252.