2023 年 8 月 28 日，英国空中交通管制运营商 NATS遭遇重大技术事故。BBC 报道称，有2000 多个航班被取消，损失估计超过1 亿英镑。该事件可能影响了数十万人。
导致事件发生的一系列事件的起始点可以追溯到将飞行计划输入飞行规划系统的时间点。
[航空公司]将计划提交至欧洲管制中心的综合初始飞行计划处理系统 (IFPS)。[..]
如果提交的飞行计划被 IFPS 接受，即符合 IFPS 规定的参数[......]，则航班在获得当地空管批准后即可起飞。飞行计划将由 IFPS 发送给需要管理该航班的所有相关 ANSP。[..]
在 Swanwick 中心的 NATS En-route 操作中，数据将被传递到 FPRSA-R。FPRSA-R 子系统将从 IFPS 接收到的数据（ATS 数据交换演示格式，ADEXP）转换为与英国国家空域系统 (NAS) 兼容的格式。NAS 是飞行数据处理系统，包含所有相关空域和航线。[..]
FPRSA-R 有一个主系统和备份系统，分别由专门的控制和监控系统（C&M）和一个汇总的中央控制和监控系统监控。此外，NAS 还存储了 4 个小时以前提交的飞行数据，以便在自动处理飞行数据功能丧失的情况下继续运行。[..]
除了备份系统提供的技术恢复能力和存储的 4 小时飞行数据外，还提供运行应急能力，以便继续提供安全服务。这是通过使用手动输入系统将飞行数据直接手动输入 NAS 的能力提供的。
总而言之：
- 飞行计划首先提交给欧洲范围内的权威机构 IFPS。
- 如果计划被接受，航班就可以起飞。
- NATS 要求在飞机进入英国领空前至少 4 小时将飞行计划转交给他们。这应该是为了给 NATS 4 小时的时间来解决处理飞行计划中的任何问题。
- 似乎还有一些程序会将飞行计划推迟到临近截止日期（见下文）。这可能是为了避免过早的飞行计划或大量日后可能变更的计划造成系统拥堵。尽管如此，这还是导致 NATS 有时在航班起飞数小时后才收到飞行计划。
ICAO 代表国际民用航空组织，是一个联合国机构。ICAO4444 飞行计划如下所示：
(FPL-TTT123-IS |
此类消息采用的格式适合机器阅读，但必要时也可供人类阅读。该格式在 PDF 的很多页中都有规定，但大致如下：
( FPL-ACID-Flt Rules Flight Type |
路由部分（本例中为N0440F310 SSOXS5 SSOXS DCT BUZRD DCT SEY DCT HTO J174 ORF J121 CHS EESNT LUNNI1）编码总速度（此处 N0440 表示 440 节）、总高度（此处 F310 表示 "飞行高度 310"，即 310 × 100 英尺（也可以是公里））、以及一连串的航点（以名称为参照），并说明如何从上一个航点到达下一个航点，通常是以名称为参照的 "已知航线"。
飞行计划被 IFPS 接受[......]。
飞机获准于 04:00 起飞。[..]
08:32 时，NATS 的 FPRSA-R 子系统从 Eurocontrol 的 IFPS 系统接收到飞行计划。这符合上述 4 小时规则。FPRSA-R 软件的目的是提取飞行计划中的英国部分。
由 IFPS 发送至 FPRSA-R 的飞行计划由 [...] ICAO4444 转换为 [...] ADEXP。ADEXP 是欧洲范围内的飞行计划规范，除其他数据外，还包括欧洲区域内特定于飞行路线的附加地理航点。对于在英国领空过境而非在英国降落的航班而言，这将包括在英国领空外飞行所需的额外航点。经过转换后，ADEXP 版本的飞行计划除其他方面外，还包括 ICAO4444 原始飞行计划以及额外的航点列表和其他数据。
ADEXP 看起来像这样：
-TITLE IFPL |
ADEXP 航路点计划包括沿其路线的两个航路点，这两个航路点地理位置不同，但具有相同的指示符。
这意味着有两行：
-PT -PTID RESIA -FL F330 -ETO 170729080731 |
具有相同的PTID字符串，如"RESIA".
尽管国际民航组织和其他机构一直在努力消除非唯一的航路点名称，但世界各地仍存在重复的航路点名称。为了避免混淆，最新标准规定，此类相同的指示符应在地理上广泛分布。在这一特定事件中，两个航路点均位于英国境外，一个朝向路线的起点，一个朝向路线的终点；相距约4000海里。
收到 ADEXP 文件后，FPRSA-R 软件开始根据 ADEXP 飞行计划在航路点信息中搜索英国空域入口点，从该航路点数据的第一行开始。FPRSA-R 能够明确识别 ADEXP 飞行计划文本中出现的字符串。
编程风格非常命令。此外，描述听起来像是程序直接处理飞行计划的文本表述，而不是从文本文件中解析出的数据结构。这一点很令人担忧，但也可能只是解释的方式不同而已。
在正确识别了进入点之后，软件继续在航点数据中搜索英国空域的出口点。
完成这些步骤后、
这部分代码在 ADEXP 航点列表中识别出英国领空的进入和退出航点。
然后，FPRSA-R 将搜索 ADEXP 文件中的 ICAO4444 部分。
看来此时，在从 ADEXP 航点列表中识别出进入和退出点后，它将尝试从 ICAO 航线中提取飞行计划的英国部分。
它首先从该数据的开头开始搜索，以找到确定的英国空域进入点。该点已成功找到。接下来，它从该部分的末尾向后搜索，以找到英国空域的出口点。该点未出现在飞行计划的该部分中，因此搜索未成功。由于不要求飞行计划包含飞行情报区（FIR）或国家空域的出口航点，因此该软件可应对这种情况。
因此，在没有明确包含英国出口点的情况下，软件逻辑会利用 ADEXP 文件中详细说明的航点来搜索英国出口点以外的下一个最近点。这一点也不存在。
因此，软件转到下一个航点。
好吧，我想事情是这样的，情况是这样的：
4 2 8 5 1 9 |
在这里，ICAO 航线的航点（用大写字母表示）被已知航线（数字）隔开。底部是 ADEXP 航点。位于英国领空的 ADEXP 航点标有 UK 字样。
- 软件已识别：入口entry：T 航点 出口exit：ADEXP 航点中的航点 W。
- 软件在 ICAO 飞行计划中找到航点 T。
- 软件未在 ICAO 飞行计划中找到航点 W。
- 因此，软件在 ADEXP 列表中选择下一个航点，即 B，并尝试找到它，但也没有找到。
- 于是，软件再次使用航点 Q 进行搜索，结果确实找到了，但却是在国际民航组织飞行计划的起始点，即飞机进入英国之前。
- 这次搜索成功了，因为飞行计划中出现了一个重复的标识符。
软件应该怎么做呢？Q显然不是我们要搜索的航点，我们要搜索的是航点Y，因为[T, O, P, Y]是国际民航组织计划中包含所有英国航点的最小段。
这里需要注意的是，原始算法存在缺陷；完全有可能明确提取出该飞行计划示例中的英国部分；见下文。导致崩溃的飞行计划很可能也是这种情况。
软件在找到入境点和出境点（后者是重复的，因此在地理位置上是不正确的）后，无法提取这两点之间有效的英国部分飞行计划。这就是事故的根本原因。因此，我们可以排除任何与网络有关的因素。
听起来异常是在代码的后一部分出现的，该部分将计划转换为 NAS 的内部格式。这部分失败的原因是，确定的进入/退出航点甚至没有指定国际民航组织航线的有效航段。
安全关键软件系统的设计宗旨是始终安全地发生故障。这意味着，一旦系统无法以明显安全的方式运行，就会进入需要人工干预的状态。
我们不禁要问，如果错误识别的航点位于更合理的地理位置，代码是否就不会出现异常并将错误数据传递给 ATCO。
在这种情况下，FPRSA-R 子系统中的软件无法确定一个合理的行动方案来保护安全，因此引发了严重异常。从广义上讲，严重异常是在探索了所有其他处理方案后的最后手段。临界异常可能是由于软件逻辑或硬件故障引起的，但本质上是受影响系统无法继续运行的标志。
听起来软件在编写时似乎认为这种异常永远不会发生。
显然，处理这种特定逻辑错误的更好方法是让 FPRSA-R 识别并删除信息，避免出现严重异常。然而，由于飞行数据是传递给 ATCO 的安全关键信息，系统必须确保其正确性，而在这种情况下却无法做到这一点。因此，系统停止了运行，避免了向管制员传递错误数据的机会。现在对软件进行修改后，在这些特殊情况下就不需要再提出关键异常了。
FPRSA-R 主系统在发出严重异常后，会在系统日志中写入一个日志文件。然后，它正确地将自己置于维护模式，C&M 系统识别出主系统已不可用。如果主系统发生故障，备用系统将无缝接管处理工作。在这种情况下，备用系统接手处理飞行计划信息。在复杂的实时系统中，备份系统软件通常位于独立的硬件上，有独立的电源和数据馈送。
因此，在接手主服务器的工作时，备份系统对飞行计划采用了相同的逻辑，结果也是一样。随后，备份系统出现了自己的严重异常，向系统日志中写入了一个日志文件，并将自己置于维护模式。
此时，由于 FPRSA-R 的主用和备用子系统都发生了安全故障，FPRSA-R 已无法自动处理飞行计划。它需要通过人工干预恢复正常服务。从收到 ADEXP 信息到主、备份子系统进入维护模式，整个过程不到 20 秒。因此，08:32 标志着飞行计划的自动处理停止，以及 4 小时缓冲到手动飞行计划输入的开始。
然后，支持团队尝试修复问题，但不幸的是，修复时间超过了他们的 4 小时：
通过直接监控运行系统的 C&M 系统以及当时使用 FPRSA-R 子系统的运行团队的直接反馈，一线支持团队得到了事故警报。团队的初步响应遵循标准恢复流程，使用集中式 C&M 系统重新启动子系统。在多次尝试恢复服务未果后，二线工程团队被调动起来，通过视频连接为现场工程师提供远程支持。
值班团队与现场工程团队一起进行了远程分析，采用了越来越详细的程序来尝试解决问题，但都没有成功。按照标准的升级程序，二线工程师参与其中，以提供进一步的高级诊断和记录功能。
虽然没有说花了多长时间，但最终还是给 FPRSA-R 系统的制造商打了电话：
由于一线和二线支持无法恢复服务或确定准确的根本原因，因此向技术设计团队和子系统制造商请求了额外支持，这很不寻常。制造商能够提供进一步的专业知识，包括分析底层软件日志，从而确定可能导致软件异常的飞行计划。通过了解导致事故的飞行计划，制造商能够提供以可控和安全的方式恢复系统所需的精确操作顺序。
系统最终得以恢复，但不幸的是，此时的连锁反应已经是灾难性的了。
制造商是一家奥地利公司 Frequentis AG：
FPRSA 子系统在 NATS 中已存在多年，2018 年，先前的 FPRSA 子系统被全球领先的空管系统供应商之一 Frequentis AG 制造的新硬件和软件所取代。该制造商的空管产品在约 150 个国家运营，在航空信息管理 (AIM) 和信息处理系统方面处于世界领先地位。
没有人会因为雇用埃森哲公司而被解雇 "的辩护。
我们可以在 Frequentis AG 的招聘页面上找到一些与空中交通管制系统相关的招聘广告：Ada、C++、Java、Python，其中 Java 最常用。上述代码听起来可能是用上述任何一种语言编写的，但 Ada 至少在其他方面比其他语言更安全。
总结
出错的原因：
- 处理飞行计划的软件 ( FPRSA-R) 是以有缺陷的方式编写的。
- 软件和系统没有经过适当的测试。
- 系统FPRSA-R有不良的故障模式
软件有错误：
- 软件无法提取国际民航组织飞行计划的英国部分，尽管该飞行计划显然是有效的（至少根据 IFPS 是这样）。
- 这个过程非常繁琐，并且由于一个愚蠢的原因而失败了。
- 航路点标记并非全球唯一，但这是一个已知问题，因此 NATS 应确保其系统足够强大以处理该问题。所有其他空中交通管制机构都必须处理这个问题。
可能缺乏形式验证？
像空中交通管制这样对安全至关重要的东西显然没有使用形式验证、模型检查等经过验证的技术来完全消除此类错误。
就像作为一个行业，我们使用 TLA+ 来阻止 AWS 停机或 Xbox 出现段错误，但不是为了让飞机保持在空中？