新的丹佛国际机场于 11 年前启用时，堪称建筑奇迹，其高科技瑰宝本应是自动化行李处理系统。它本应自主地在 26 英里的传送带上运送行李，以便快速、无缝地交付给飞机和乘客。但软件问题一直困扰着该系统，导致机场启用时间推迟了 16 个月，并增加了数亿美元的成本超支。尽管经过多年的调整，它从未可靠运行过。去年夏天，机场管理人员最终放弃了该系统，转而使用传统的手动装载行李车和带人工驾驶员的拖车。机械处理系统的设计者 BAE 自动化系统公司被清算，其主要用户美国联合航空公司也部分因这场混乱而陷入破产。
数百万沮丧的用户每天都在为糟糕的软件设计付出高昂的代价。其他臭名昭著的案例包括美国国税局的代价惨重的惨败（1997 年耗资 40 亿美元的现代化努力失败，随后又进行了同样麻烦的 80 亿美元的更新项目）；联邦调查局（2005 年，一个耗资 1.7 亿美元的虚拟案件档案管理系统被废弃）；以及联邦航空管理局（一项长期且仍然不成功的对其老化的空中交通管制系统进行改造的尝试）。
发生如此大规模的失败是因为关键的设计缺陷发现得太晚了。只有在程序员开始构建代码（计算机用于执行程序的指令）之后，他们才发现其设计的不足之处。有时，致命的不一致或遗漏是罪魁祸首，但更常见的情况是，总体设计含糊不清且考虑不周。随着代码随着零星的修复而增长，详细的设计结构确实出现了——但它是一个充满特殊情况和漏洞的设计，没有连贯的原则。就像建筑物一样，当软件的基础不牢固时，由此产生的结构是不稳定的。
支持科学新闻报道
如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻报道 订阅。通过购买订阅，您正在帮助确保有关塑造我们当今世界的发现和想法的具有影响力的故事的未来。
参与备受瞩目的软件故障的管理人员可能会辩称，他们在辩护中遵循了行业标准做法，不幸的是，他们是对的。开发人员很少精确地阐明其设计并对其进行分析，以检查它们是否体现了所需的属性。但是，随着计算机现在驾驶飞机、火车和汽车，并运行着世界上大部分的金融、通信、贸易和生产机械，社会迫切需要提高软件的可靠性。
现在，新一代软件设计工具正在涌现。它们的分析引擎在原理上类似于工程师越来越多地用于检查计算机硬件设计的工具。开发人员使用高级（摘要）编码符号对软件设计进行建模，然后应用一个工具来探索系统的数十亿种可能的执行，寻找会导致系统以意外方式运行的异常情况。此过程在代码编写之前就捕获了设计中的细微缺陷，但更重要的是，它产生了一个精确、稳健且经过彻底测试的设计。Alloy 就是此类工具的一个示例，它由我的研究小组和我构建。Alloy（可在网上免费获得）已被证明在航空电子软件、电话、密码系统和癌症治疗中使用的机器设计等各种应用中都非常有用。
几乎所有严重的软件问题都可以追溯到编程开始之前所犯的概念性错误。
Alloy 和相关的设计检查工具建立在 25 年来对如何用数学方法证明程序正确性的现有研究的基础之上。但是，它们不是要求手动完成证明，而是采用自动化推理技术，将软件设计问题视为一个待解决的巨型难题。这些分析器对设计而不是程序代码进行操作，因此它们无法保证程序不会崩溃。但是，它们有可能为软件工程师提供首批实用工具，以确保设计稳健且没有概念性缺陷，从而为构建可靠的软件系统奠定坚实的基础。[中断]
评估设计
糟糕的软件不是一个新问题。早在 20 世纪 60 年代就出现了软件危机的警告，并且随着计算机融入社会结构而愈演愈烈[参见 W. Wayt Gibbs 的“软件的长期危机”；《大众科学》，1994 年 9 月]。
如今，大多数软件通常通过测试进行调试和改进。工程师使用各种各样的起始条件（或输入）运行程序，以查看其是否按预期运行。尽管这种做法可以捕获大量小缺陷，但它常常忽略软件基本设计中的缺陷。在某种意义上，这些测试程序只见树木不见森林（病态的森林）。
更糟糕的是，在测试过程中“修复”的错误通常会加剧设计问题。随着程序员调试代码并插入新功能，软件不可避免地会滋生复杂性的藤壶，从而创造更多错误和低效操作的机会。这种情况让人联想到古希腊人首先提出的（不正确的）托勒密行星运动理论。在中世纪，随着观测表明预测不准确，天文学家调整了托勒密系统，该系统依赖于本轮。当事实证明这还不够时，他们开始在本轮上添加本轮。几个世纪以来的进一步微调从未解决问题，因为最初的概念存在致命缺陷。
同样，糟糕的软件往往会变得越来越复杂，越来越不可靠，无论投入多少时间和金钱来改进它。众所周知，软件系统的严重问题很少源于编程错误；几乎所有严重的困难都可以追溯到编程甚至开始之前所犯的概念性错误。相比之下，在最初确定需求、规范或程序设计期间进行少量建模和分析的成本仅占检查所有代码的价格标签的一小部分，但却提供了从详尽分析中获得的大部分好处。尽早关注设计可以避免以后的昂贵麻烦。
软件设计工具的出现速度一直很慢，因为软件不遵守物理定律。由于计算机程序本质上是由位构建的值的数学对象，因此软件程序是离散的（粒子状的）而不是连续的。机械工程师可以用很大的力来应力部件，并假设如果它能承受住，那么当受到稍小的力时它就不会失效。当物体受到（大多是连续的）物理世界原理的约束时，一个量的微小变化通常会产生另一个量的微小变化。不幸的是，对于软件来说，没有这样的普遍性：人们无法在测试用例之间进行外推。如果一块软件可以工作，那么这一事实并不能说明类似的代码块的操作；它们是离散且独立的。
在计算机科学的早期，研究人员希望程序员能够像数学家证明他们的定理一样证明他们的编码是正确的。然而，由于无法自动化所涉及的许多步骤，人类专家不得不完成大部分工作。这些所谓的重型形式化方法是不切实际的，除非对于相对适度但特别关键的软件，例如用于控制铁路交叉口的算法。
最近，研究人员采用了一种非常不同的方法，即利用当今更快的处理器的强大功能来测试每种可能的场景。这种称为模型检查的方法现在广泛用于验证集成电路设计。其思想是模拟实践中可能出现的每种可能的状态序列（系统在特定时间的条件），并确定没有一种状态序列会导致故障。对于微芯片设计，要评估的状态数量通常非常巨大：10100 或更多。对于软件来说，挑战要严峻得多。但是，巧妙的编码技术（通过这种技术可以非常紧凑地表示大量的软件状态）使得同时考虑这些大型集合来检查每个状态成为可能。[中断]
遗憾的是，仅靠模型检查无法处理具有复杂结构的状态，这通常是大多数软件设计的特征。我的研究同事和我开发了一种方法，该方法与模型检查具有相同的精神，但采用了不同的机制。与模型检查一样，它考虑了所有可能的场景（尽管事实上，需要引入一些界限来保持问题的有限性，因为软件不受硬件施加的物理限制的约束）。但是，与模型检查不同，我们的技术不会一次检查一个场景的全部内容。相反，它通过以自动方式一次填充一位来搜索不良场景——导致失败的场景，并且没有特定的顺序。
在某种程度上，这个过程类似于机器人手臂将拼图游戏的每一块逐个放入到位，直到最终出现完整的图像。如果该图像对应于不良场景，则 Alloy 将完成其工作。因此，Alloy 将设计分析视为一个待解决的难题。一些其他最近开发的软件模型检查器也以这种方式工作。
解决方案是一个难题
为了理解 Alloy 如何解决软件设计难题，有必要考虑一个古老的谜题：一个农民去市场买了一只狐狸、一只鹅和一袋玉米。在回家的路上，他必须乘船将货物运过河。然而，小船一次只能容纳人和一件购买的物品。问题就在这里：如果无人看管，狐狸会吃掉鹅，鹅会吃掉玉米。那么农民如何才能将所有货物完好无损地运到对岸呢？
这种谜题涉及到找到满足一系列约束的场景。我们在头脑中通过想象一系列步骤来完成这项任务：农民首先运送鹅；在下一次旅行中，他带走狐狸，然后他带回鹅，然后，将鹅留在后面，带着玉米过河；然后他返回去取鹅。通过检查每个步骤是否满足约束，我们确保每件物品都保持安全。
成功的软件设计施加了类似的规则数组，尽管要复杂得多。为了有用，设计检查工具必须能够找到反例：难题的解决方案，这些解决方案满足所有“好的”约束（因此可能在程序运行时发生）和一个额外的“坏的”约束（因此产生不可接受的结果）。如果出现任何此类反例，它们将揭示设计中的缺陷。因此，虽然谜题解决者很高兴找到“农民困境”的解决方案，但软件设计难题的解决方案是坏消息：这意味着存在不良场景，并且设计有缺陷。在实践中，反例本身可能不会导致任何问题。它可能反而揭示了设计者最初如何描述不可接受的结果的差异。无论哪种方式，都需要修复某些东西——设计或设计者的期望。
其思想是模拟软件可能采取的每种状态，以确定没有一种状态会导致故障。
搜索反例的最大困难在于，即使是中等复杂度的软件设计中，潜在场景的数量通常也很大，但只有一小部分对应于反例。想象一下试图计划谁在婚宴上坐在谁旁边。如果所有与会者相处融洽，则解决方案是微不足道的。加入一些需要分开的前配偶，问题就变得棘手了。现在考虑一下罗密欧和朱丽叶招待会的座位表。如果有 20 个座位，并且 10 位客人中的任何一位都可以坐在每个座位上，那么就有 1020 种可能的组合。即使每秒检查 10 亿个场景，计算机也需要 3000 年才能探索完所有场景。
在 20 世纪 80 年代，研究人员将这种形式的问题识别为一类特殊的问题，在最坏的情况下，只能通过枚举所有可能的场景来解决。但在过去的十年中，随着新的搜索策略和算法以及不断增长的计算能力的构建，研究人员开发了称为 SAT（可满足性）求解器的工具，这些工具可以相当容易地处理这些问题。现在许多工具都可以免费获得，并且通常可以解决具有数百万个约束的问题。[中断]
抽象的重要性
顾名思义，Alloy 融合了两个有助于使软件设计更健壮的元素。一种是新的语言，它有助于阐明软件设计的结构和行为。另一种是自动化分析器（它结合了 SAT 求解器），用于筛选大量可能的场景。
应用 Alloy 的第一步是创建设计模型：不是软件工程中典型的粗略草图或流程图，而是一个精确的模型，它详细说明了系统的“移动部件”和特定行为，包括所需的和不需要的行为及其组件。软件工程师首先写下设计中各种对象的定义，然后将这些对象分组为数学集合：结构和行为相似的事物的集合（例如，所有凯普莱特的集合）并通过数学关系（例如，将彼此相邻的客人关联起来的关系）链接在一起。
接下来是约束这些集合和关系的事实。在软件设计中，事实包括软件系统的机制以及关于其他组件的假设（例如，关于人类用户预期行为的陈述）。其中一些事实是简单的假设——例如，没有人既是凯普莱特又是蒙太古，并且每个客人恰好坐在另外两位客人旁边。其中一些事实反映了设计本身：例如，在我们的座位规划器中，规则是每张桌子（除了主桌）都分配给一个家庭或另一个家庭。
Alloy 揭示了已发布软件设计中的严重缺陷。
最后，还有断言，它们是预期从事实中得出的约束。在我们的示例中，除了罗密欧和朱丽叶之外，任何凯普莱特都不应坐在蒙太古旁边。断言表明，系统永远不会进入某些不良状态，并且特定的不良事件序列永远不会发生。
Alloy 的分析器组件利用 SAT 求解器搜索反例——软件系统的可能场景，这些场景在其设计允许的范围内，但未能通过健全性检查（通过编写如果模型设计正确则必须为真的断言来完成）。换句话说，该工具试图构建满足事实但违反陈述断言的情况。在我们的例子中，它会生成一个座位安排，其中凯普莱特（朱丽叶除外）坐在主桌的蒙太古（罗密欧除外）旁边。要修复座位规则，我们可以添加一个新事实：罗密欧和朱丽叶独自占据主桌。现在 Alloy 将找不到反例。
集合和关系、事实和断言的声明共同构成了一个抽象，它捕捉了软件设计的本质。写下所有这些内容使设计的局限性变得明确，并迫使工程师认真思考哪些抽象最有效。糟糕的抽象选择是许多不必要的复杂或不可靠系统的根源。
依赖于基于简单而健壮的抽象构建的软件的系统也应该更易于使用。考虑一下电子票务如何简化航空旅行，通用产品代码如何使购物更轻松，或者基于 800 号码的电话会议如何使电话会议更可行。这些创新都源于底层软件中体现的基本抽象的转变。
可靠性之路
类似于 Alloy 的工具目前主要用于研究和前沿工业环境中。该技术已被用于探索电话交换系统的新架构，设计针对黑客攻击的安全航空电子处理器，以及描述通信网络的访问控制策略。我们已使用它来检查广泛使用且稳健的软件设备，例如用于在网络上查找打印机的协议和用于在机器之间同步文件的工具。[中断]
此外，Alloy 还揭示了已发布软件设计中的严重缺陷——例如，一种密钥管理协议，该协议本应根据组成员身份强制执行特殊访问规则，但结果却授予了本应被拒绝的前成员访问权限。值得注意的是，许多使用过 Alloy 的程序员对该工具在即使是最简单的应用程序的设计中也发现如此多的缺陷感到惊讶。
工具像 Alloy 一样被行业更广泛地采用可能只是时间问题。底层 SAT 求解器的改进将使分析工具更快、更好，并且能够处理非常大的系统。与此同时，新一代接受过这些方法教育的软件设计师将把它们融入到他们的工作中。建模越来越受欢迎，尤其是在迫切希望看到软件系统设计的某些描述（超出代码本身）的管理人员中。
在某个时候，可能会出现软件对我们的日常基础设施变得至关重要，以至于社会将不再容忍糟糕的软件。因此，政府甚至可能制定检查和许可法规，以强制执行高质量的程序构建技术。也许有一天，软件系统将真正通过设计实现稳健、可预测且易于使用。