新的丹佛國際機場於 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 求解器的改進將使分析工具更快、更好，並且能夠處理非常大的系統。與此同時，新一代接受過這些方法教育的軟體設計師將把它們融入到他們的工作中。建模越來越受歡迎，尤其是在迫切希望看到軟體系統設計的某些描述（超出程式碼本身）的管理人員中。
在某個時候，可能會出現軟體對我們的日常基礎設施變得至關重要，以至於社會將不再容忍糟糕的軟體。因此，政府甚至可能制定檢查和許可法規，以強制執行高質量的程式構建技術。也許有一天，軟體系統將真正透過設計實現穩健、可預測且易於使用。