什么是 formal methods

“Formal methods” 是计算机科学中的一个术语，它指的是一种使用数学模型和技术来描述和分析计算机系统的方法。这种方法尤其适用于设计、开发和验证复杂的软件和硬件系统。

“Formal methods” 可以帮助开发人员理解系统的行为，并在系统开发过程中发现潜在的问题和错误。这些方法通常包括：规范语言（用于描述系统应该做什么），建模语言（用于表示系统的结构和行为），以及验证技术（用于证明系统满足其规范的属性）。

尽管 formal methods 能够提供严格的正确性保证，但其使用也存在一些挑战，例如可能需要较高的数学技能，且往往需要较大的时间和资源投入。因此，实际中并不是所有的项目都会使用 formal methods，但在需要确保高可靠性和安全性的领域（如航空航天、医疗设备和核能设施等），它们的应用尤为常见。

案例1：造影机器

背景：塞拉皮姆25号是一台在1980年代部署的辐射治疗机。它由一台被视为复古的PDP 11机器驱动，这台机器在UNIX历史中颇有知名度。这台治疗机主要通过发射高能辐射束来治疗癌症。

• 问题：塞拉皮姆25号的使用导致多人因辐射过量而死亡。其中一个案例是在1986年，一名叫科克斯的患者在接受治疗时被击中了极强的辐射束。他尝试站起来，但操作员再次运行了机器，他被第二次击中。他试图逃跑并敲打连接治疗室和控制室的门，但他最后还是因过量辐射在五个月后死亡。
• 系统的缺陷：塞拉皮姆25号的软件经常出现错误信息，这导致它并不是一个特别可靠的设备。另外，它的用户界面是一个文本终端，只有黑白两种颜色，操作员只能通过键盘进行操作。在这个界面上修改指令很复杂，需要移动光标删除并替换字母，这样的设计几乎就是在鼓励出错。
• 安全机制的问题：在25号之前，塞拉皮姆公司生产的前两代辐射治疗机中，有硬件机制防止对人体施加过量辐射。但是在25号上，他们决定用软件替代这些硬件机制，他们过于自信地认为软件可以完全控制机器并保证不会出问题。
• 制造商的态度：即使发生了问题，制造商最初拒绝承认他们的机器存在问题，因此机器并未立即停用，这导致更多的人受到了伤害。
• 与现代问题的相似性：在当前的一些案例中，我们可以看到类似的问题。例如，在特斯拉的自动驾驶软件的问题中，也存在过度自信软件的情况，导致没有足够的安全防护措施。

案例2： 特斯拉汽车的自动驾驶功能

• 有关特斯拉汽车的讨论主要集中在其自动驾驶功能，特别是对其安全性的考量。以下是关于特斯拉汽车的主要描述和思考：
• 过度自信的问题：特斯拉在其自动驾驶软件中的过度自信。特斯拉的工程师可能过于相信他们的自动驾驶软件能力，忽视了额外的安全特性的重要性。这种过度自信可能导致了不必要的风险，可能导致了一些致命的事故。
• 安全功能的缺失：文中提到，特斯拉的自动驾驶系统被设计为可以在任何时候被驾驶员干预。然而，这个设计似乎预设了驾驶员会始终保持警觉并及时干预，而这可能与现实中驾驶员使用自动驾驶功能的心理反应不符。如果驾驶员对自动驾驶功能产生过度依赖，可能会导致警觉性降低，从而影响安全。
• 人性化设计的缺乏：许多其他自动驾驶汽车制造商考虑到了人性化的设计，比如通过监控系统确保驾驶员始终保持警觉，如果驾驶员开始昏睡或者没有将目光放在路上，这些系统将关闭自动驾驶功能。然而，特斯拉的自动驾驶系统似乎没有完全采用这样的设计。
• 这些思考和讨论对于任何正在研发或使用自动驾驶系统的人或组织都是非常重要的，因为它们提醒我们要保持对于这些系统能力的清晰理解，同时也要认识到额外的安全防护措施的重要性。

案例3：空客 320

• 这段内容描述了一次涉及空客A320的飞行事故。空客A320是第一架采用飞行电缆（Fly-by-Wire）系统的民用飞机。在这个系统中，飞机上的控制操作并不直接影响物理作动器，而是生成电子信号，通过网络传送到飞机的其他部分，然后触发某个作动器。简单来说，飞机被构建为一个大型的分布式系统或网络系统，其中有许多小型计算机相互通信。
• 然而，在A320的首次载客飞行中，发生了一起严重的事故。在苏格兰的一个航展上，这架飞机进行了一次低速低空飞行的演示，以展示飞行电缆技术的精密度。然而，飞机飞得太低，没有及时升高，最终撞上了树并坠毁。这次事故造成一名女士和两名儿童丧生。
• 关于这起事故的原因，人们有不同的看法。官方的报告认为是飞行员操作失误导致的事故，飞行员飞得太低、太慢，没有看到树林。然而，飞行员则坚称是飞行电缆系统的问题，这个系统阻止了飞机在正确的姿态下稳定，并指出还有其他因素，比如他们并不知道那片森林的存在，因为在他们得到的地图上并没有标出，而且他们原本预计的是一个更长的跑道。
• 这个例子的重要教训是，事故的发生往往不仅仅是单一的故障导致的，而是一系列因素的相互作用结果。我们需要考虑系统运行的上下文环境，包括操作系统的人员，并对他们可能的行为做出合理的假设。

案例4：波音737

• 这是关于波音737 Max的案例。这款飞机在几年前发生了一些事故，导致飞机停飞了很长时间进行调查，并于2020年和2021年根据不同地区的规定重新获得了飞行许可。事故中发生了两次重大的波音737 Max飞机坠毁，一次是在2018年10月29日的狮子航空的航班，几个月后，埃塞俄比亚航空的航班也发生了坠毁，两次坠机均为同型号飞机。两次坠机事件导致346人死亡。
• 调查发现，尽管存在许多可能的影响因素，但最核心的因素似乎是737 Max飞机上安装的一个名为MCAS的软件系统。MCAS是为了解决737 Max比前代飞机更大的发动机所引起的飞行特性改变的问题。737 Max比之前的73-7飞机的发动机更大，这就改变了飞机的气动特性。因此，他们必须安装一个软件系统来弥补不同的发动机对飞机飞行方式的影响。
• MCAS系统的目标是在飞机的鼻子开始过多地向上指时检测并调整，以防止飞机的鼻子过度上扬。当检测到飞机鼻子过度上扬时，系统会自动使飞机鼻子下降，以平稳飞机，并防止发动机熄火。然而，如果飞机鼻子的角度传感器向飞行控制电脑传送错误的数据，那么这个系统可能会反复激活。这似乎就是这两次坠机事件的原因。这个系统在接收到错误的角度信息后，就会反复激活，使飞机鼻子反复下降，最终导致飞机坠地。
• 另一个问题是，飞行员没有得到关于这个MCAS系统的培训，甚至根本没有被告知它的存在，因此他们不知道如何覆盖它。而波音在设计这个系统时，做了一些关于飞行员可能如何反应的假设，但飞行员并没有按照这些假设进行操作，这也是系统失败的原因之一。
• 一些决策也导致了这个悲剧的发生，比如，为了使飞机更经济有效，他们决定安装更大的发动机，并且为了避免重新进行昂贵的认证过程，他们只使用一个

以下是详细的总结：

• 关于文化：文化在软件领域（以及特斯拉等公司）中起着决定性的作用，影响着决策。在波音737 MAX的案例中，一种观点是，他们可能优先考虑了经济利益而非安全。
• 对波音737 MAX的决策的概述：
• 波音为了提高飞机的经济效益，通过装载更大的发动机来提高燃油效率，因此安装了MCAS系统。
  为了节省飞行员的再培训成本，波音并未告知飞行员MCAS系统的存在，也未更新训练资料。
  波音没有采用多个攻角传感器，可能是为了避免重新进行飞行控制认证。
• 安全分析：波音决定了MCAS系统不能导致大规模的故障，因此没有采用冗余输入。他们认为该系统可能对飞机的飞行产生一些影响，但飞行员始终可以覆盖它，这种影响不会过大。然而，实际情况证明他们是错误的。
• 后果：除了已经讨论过的346人死亡之外，这些飞机被无限期停飞了三四年，这是美国航空史上最长的停飞记录。此外，波音公司的损失大约在200亿美元左右，他们的首席执行官也下台了。由于连续的重大事故，很多航空公司取消了订单，这也让波音损失了大约200亿美元的收入。
• 教训：从中可以学到几个教训，一个是关于文化的，另一个是关于贪图小便宜可能会让你长期付出代价。这个案例证明了一个老式的工程格言，即做一件事情最便宜的方式就是一开始就做对，而不是回头去改。
• 文化和伦理：所有的工程师都有责任以伦理的方式行事。如果你在的公司将挣钱优先于道德行事或安全行事，那么你设计和实施的技术可能会对人们造成伤害。
• 关于职业道德的呼吁：这段讲话最后呼吁听众，在他们的职业生涯中，应该记住这些失败的教训，思考他们所做的决定可能对人们的生活产生巨大的影响。