关于支持科学新闻
如果您喜欢这篇文章，请考虑订阅我们的获奖新闻，以支持我们的工作。 订阅。 通过购买订阅，您将帮助确保关于当今塑造我们世界的发现和想法的具有影响力的故事的未来。
现代医疗设备几乎在各个方面都依赖软件运行。在用于癌症治疗的机器中，即使是“紧急停止”按钮也不是一个实际的电子开关，而是一个软件程序：按下它会导致大约15,000行代码执行并关闭系统——当然，除非软件中存在错误或设计缺陷。这就是 Alloy 的用武之地——它分析程序以发现设计问题。
例如，在与癌症治疗系统的开发人员合作时，我们使用 Alloy 来探索其某些功能的设计。在一种情况下，我们采用了一个新的调度系统的设计，该系统决定将光束发送到哪个治疗室。我们设置 Alloy 来查找主控制室的操作员和治疗室的治疗师之间的交互会产生意外结果的场景。Alloy 发现了各种最初未曾预料到的场景。
在另一种情况下，我们将 Alloy 应用于患者在质子束下定位的复杂协议的设计，结果发现它有一个微妙而意外的后果：即使在没有有意调整的情况下，机架的角度也会随着时间的推移而缓慢改变。通过一个小的 Alloy 模型，我们展示了如何通过选择正确的抽象，将这个问题简化为一个与设计一个记住驾驶员座椅位置的汽车配件系统相同，相当简单的问题。事实上，治疗系统有很多安全措施，机架移动并不是一个危险的问题。但是，如果从一开始就使用了正确的抽象，设计就会简单得多，并且操作软件也会容易得多。