關於支援科學新聞
如果您喜歡這篇文章，請考慮訂閱我們的獲獎新聞，以支援我們的工作。 訂閱。 透過購買訂閱，您將幫助確保關於當今塑造我們世界的發現和想法的具有影響力的故事的未來。
現代醫療裝置幾乎在各個方面都依賴軟體執行。在用於癌症治療的機器中，即使是“緊急停止”按鈕也不是一個實際的電子開關，而是一個軟體程式：按下它會導致大約15,000行程式碼執行並關閉系統——當然，除非軟體中存在錯誤或設計缺陷。這就是 Alloy 的用武之地——它分析程式以發現設計問題。
例如，在與癌症治療系統的開發人員合作時，我們使用 Alloy 來探索其某些功能的設計。在一種情況下，我們採用了一個新的排程系統的設計，該系統決定將光束髮送到哪個治療室。我們設定 Alloy 來查詢主控制室的操作員和治療室的治療師之間的互動會產生意外結果的場景。Alloy 發現了各種最初未曾預料到的場景。
在另一種情況下，我們將 Alloy 應用於患者在質子束下定位的複雜協議的設計，結果發現它有一個微妙而意外的後果：即使在沒有有意調整的情況下，機架的角度也會隨著時間的推移而緩慢改變。透過一個小的 Alloy 模型，我們展示瞭如何透過選擇正確的抽象，將這個問題簡化為一個與設計一個記住駕駛員座椅位置的汽車配件系統相同，相當簡單的問題。事實上，治療系統有很多安全措施，機架移動並不是一個危險的問題。但是，如果從一開始就使用了正確的抽象，設計就會簡單得多，並且操作軟體也會容易得多。