目標與問題：程式錯誤的挑戰
我將會談論，當然，是關於模型檢驗，並且我會提供一些個人視角。那麼，我們的最終目標是什麼？不必然是形式化驗證本身。而是關於如何編程，也就是如何編寫可預測且可靠的程式。在這裡，「程式」是一個廣義詞，涵蓋了硬體設計、軟體程式、系統、嵌入式系統等等。而關鍵問題在於電腦程式存在錯誤，我們俗稱「臭蟲 (bugs)」。
有各種嘗試開發優秀程式的策略。其中之一是使用具有進階且複雜功能的程式語言，讓人類程式設計師更容易寫出好的程式。另一種是測試，試圖系統性地找出臭蟲；還有模擬工具，讓程式執行一段時間，並以某種系統化的方式觀察會發生什麼。我們透過模型檢驗所追求的解決方案，屬於形式化方法 (formal methods) 的類別，其基礎是數學邏輯。
然而，並非所有程式都會提交給形式化驗證或模型檢驗，因為應用驗證工具可能既困難又昂貴。因此，它們通常應用的範疇是安全性關鍵系統或具有重要經濟價值的應用。
形式化方法與應用範疇：慘痛的錯誤案例
好吧，我們有一系列眾所周知的惡名昭彰的臭蟲。有歐洲的 Ariane 5 火箭，由於軟體溢位錯誤而爆炸，造成了 5 億美元的損失。有 USS Yorktown 號驅逐艦，它使用了一些現成的商業軟體。一位水手在其中一個商業程式中輸入了一個零。這導致了溢位。該電腦崩潰了。崩潰蔓延到船上的其他機器，導致驅逐艦完全停擺。情況實際上可能相當嚴峻。曾經險些釀成核戰。1960 年 10 月 5 日，美國的飛彈防禦早期預警系統軟體將月亮誤認為是即將來襲的飛彈攻擊，這當然可能導致美國的反擊，以及我想是核冬天。幸運的是，當時還有人的介入。還有 Pentium 錯誤。還有 Therac-25 放射治療機，它在腫瘤治療中應該有利地照射患者，但由於軟體錯誤，它過度照射了患者，並導致多人死亡。
這裡的主要思想是，電腦無處不在，所以它們最好能正常運作。不幸的是，臭蟲普遍存在。電腦程式的正確行為至關重要，而驗證似乎是獲得正確行為的最佳途徑。
模型檢驗：核心概念與貢獻
模型檢驗，作為一種特定的驗證形式，相當於在狀態圖中搜尋時態模式，儘管存在狀態爆炸問題，它仍然有效。其關鍵屬性在於模型檢驗演算法的效率以及斷言語言的表達能力。
模型檢驗至今對全球的長期貢獻是，我們今天確實 在 執行驗證。二十、三十年前，我們只是 談論 驗證。值得注意的是，模型檢驗已經取代了證明的必要性，而三十年前，證明是形式化驗證的一個重要方面。
挑戰：複雜性與軟體驗證
挑戰是什麼？我們需要更好地應對複雜性。我們需要更好的擴展性，而且我認為重大的挑戰是軟體驗證。軟體程式比硬體設計大得多，而且它們具有複雜的動態狀態。
歷史背景：從公理化驗證到時態邏輯
回到 1980 年代初期，當模型檢驗被構思出來時，主流的驗證框架是 Floyd-Horstall 公理化驗證。人們主要針對循序程式進行手動證明其正確性。這些證明既繁瑣又困難，並且需要獨創性才能想出像迴圈不變式這樣的東西。學術上，這項工作是成功的。它提出了組成性 (compositionality) 的重要思想——分而治之，以及證明系統的健全性 (soundness) 的概念，以及完備性 (completeness) 的有趣概念。並且有一些成功的例子，但不是針對小型程式。你可能會有一頁或半頁的程式，卻需要多頁的證明。它從未擴展到大型程式或工業級程式。問題在於想出這些證明實在太困難了。
因此，在我們看來，應該有一種更簡單的方法。而這條道路指向了模態時態邏輯 (modal tense logic)，也稱為時態邏輯 (temporal logic)，Amir Pnueli 在他 1977 年的基礎論文中指出了時態邏輯非常適合於推理關於持續執行的並行程式，例如作業系統、網路協定、機載航空電子設備系統，這些系統今天我們稱之為反應式系統 (reactive systems)。
現在，存在這樣一個理論事實：任何一致的時態邏輯規約 F 都可以在一個小的有限模型 M 中實現，這個模型是一個小的狀態圖。而且在實踐中，許多並行程式是有限狀態的，至少如果你考慮它們的同步骨架，並排除循序程式碼和關鍵區段等等。
模型檢驗：從理論到實踐的提案
這就導致了模型檢驗的思想。給定任何有限狀態圖 M 和規約 F，檢查 M 是否是規約 F 的真正模型。這表示為 M $\models$ F。在結構 M 或狀態圖 M 中，規約公式 F 為真。
因此，在 80 年代早期，Ed Clark 和我以及 Joseph Sifakis 與 Bernard Queille 提出了模型檢驗，這是一種自動驗證有限狀態並行系統正確性的方法。規約語言是時態邏輯，它提供了描述隨時間變化的有用形式主義。底層方法在某種意義上對狀態圖的大小是有效的，並且提供了對狀態圖的靈活搜尋，以查看時態邏輯中指定的某些模式是否成立。它是針對有限狀態系統的。結果證明它是演算法化的，並且旨在實用，隨著時間的推移，這已被證明是真實的。
時態邏輯描述了並行程式的持續行為。在線性時態邏輯 (linear temporal logic) 中，你有操作符號，例如 F P（有時候 P），沿著時間線或計算過程 P 為真；總為 P 或 G P（永遠 P），在計算過程中的所有時刻 P 都為真。如果你想利用程式通常與非確定性相關的事實，那麼時間可以被視為分支的，如果 H 是一個線性時間公式，你可以區分 A H（沿著所有未來的計算 H）和 E H（沿著某些未來的計算 H）。
現在我提出以下主張。雖然效率和良好的複雜度至關重要，但時態邏輯及其表達能力是關鍵，可以說是模型檢驗成功的關鍵因素。我的意思是，在實踐中，你有一種邏輯，它有一些基本的時態操作符號，你可以通過將這些時態操作符號與布林連接詞組合來創建幾乎無限的斷言，並且在原始時態邏輯的情況下，它與自然語言相關，我認為這有助於人類理解，更普遍地說，如果你要使用驗證方法來檢查正確性屬性，你必須能夠表達你想說的話。規約語言必須足夠富有表達能力。如果不是，那還有什麼意義呢？
時態邏輯的類型與重要性
存在許多時態邏輯和形式主義。這裡列出一些關鍵的。在分支時間邏輯 (branching time logic) 的類別中，CTL (Computation Tree Logic)，你可以說 A F P（沿著每個未來最終 P），換句話說，P 是不可避免的；你可以區分這與 E F P（沿著某些未來最終 P）。還有這種更豐富的邏輯，CTL star (CTL*)，你可以在 A 或 E 後面接任意的線性時態邏輯公式，然後進一步組合它們。結果證明 CTL 不能談論公平性 (fairness)。有一種它的版本稱為 fair CTL，可以做到。CTL* 也可以談論公平性，但會有複雜度上的損失，而 fair CTL 實際上沒有這樣的損失。對於線性時間框架，經典的線性時態邏輯，你可以說總為真：如果 P 為真，最終 Q 也為真，因此 P 導致 Q 或 P 在時態上蘊含 Q。
Omega regular expressions 是另一種線性的時態形式主義，也被證明很有用。當將它們應用於程式時，對程式的所有行為都存在一個隱含的全稱量化。線性時態邏輯很簡單。分支時態邏輯更複雜。分支時態邏輯更具表達能力，因為你可以談論可能性以及必然性。
好吧，與 mu calculus 相關的一些基礎問題和實際問題。你可以將其視為帶有最小和最大不動點運算符的 CTL。它有時被稱為「萬物理論」。Mu calculus 等價於無限樹上的有限狀態自動機。這是一個很好的衡量標準。但實際上，它的使用是許多工具實現的基礎。
然後還有工業界的時態邏輯，例如 IBM Sugar、Excella、IEEE 1850 標準的屬性規約語言 PSL (Property Specification Language)、Intel Forespec，它們是針對硬體驗證量身定制的，實際上包含許多專用宏。還有其他邏輯。我曾經與 Dijkstra 談論邏輯和程式語言，他說它們就像螞蟻，太多了。我不知道我們是否真的會有一個小的邏輯集合。
但我們可以問哪種邏輯或形式主義是最好的。這是一個非常難回答的問題，並且會不斷催生新的邏輯。首先，你應該問什麼對於什麼是最好的。關鍵標準是表達能力和便利性。其他標準還有效率、簡潔性 (succinctness)——你可以寫多短的規約來捕捉一個屬性。而且你可以某種程度上量化各種權衡，例如表達能力與效率。但便利性是一種模糊的、不完全數學化或形式化的概念。因此，人們可能會永遠為了便利性而引入新的邏輯。我的意思是，這些工業邏輯就是這樣發生的。
現在，一個有趣的事情是，至少在線性時態邏輯的框架下，低表達能力在原則上是足夠的，因為你可以將原始系統上的模型檢驗問題編碼為對替代系統的更簡單查詢。如果你使用自動機理論，它提供了一個統一的框架，涵蓋了建模、規約、模型檢驗、綜合。Vardi 和 Wolper 在 1994 年證明，線性時態邏輯，原始 LTL 和一些有趣的擴展，可以轉換為自動機。Chenlong Lei 和我在 1985 年證明，自動機的非空性 (non-emptiness) 可以被捕捉到。作為一個 LTL 模型檢驗問題，當且僅當自動機或其圖表達了類似於 E G F green 的意思時，自動機是非空的。存在一條路徑，沿著該路徑 green 是週期性發生的 (recurrent)。然後 Vardi 和 Wolper 關於用自動機進行 LTL 模型檢驗的結果，可以用遞歸來表達：給定一個系統 L M，你想檢查是否存在一條滿足 LTL 斷言 H 的路徑，那麼你可以將其轉換為詢問在另一個系統 L M' 中，是否存在一條沿著該路徑 blue 是週期性發生的？而 L M' 本質上是 L M 與 H 的自動機的同步積 (synchronized product)。Schuppan 和 Bier 的論文簡化了這一點，LTL 模型檢驗可以轉換為可達性 (reachability) 問題：L M $\models$ E H 當且僅當 L M double prime $\models$ E F blue，其中 L M double prime 是 L M prime 交叉 B，而 B 是一個自動機，它猜測 L M prime 中的一個接受循環 (accepting cycle)。
狀態爆炸問題及其解決方案
狀態爆炸 (State explosion)，狀態空間的大小可能與程式的大小呈指數關係。這就是我們說的狀態爆炸。例如，在一個有 100 台櫃員機的銀行網路中，每台櫃員機由一個 10 個狀態的有限狀態自動機控制，可能存在 $10^{100}$ 個狀態，即全域狀態。我們通常有三種方法來嘗試限制狀態爆炸。
一種是抽象 (Abstraction)。你試著將原始系統中的狀態聚類在一起，你會得到一個較小的抽象系統，有時稱為商結構 (quotient structure)。Ed 和我在我們 1981 年的原始論文中概括性地討論了這一點及其重要性。Joseph Sifakis 在 1983 年的一篇論文中以同態 (homomorphisms) 的形式將其形式化。你取原始系統，並有一個同態映射到一個較小的系統。如果原始系統中有一條壞路徑，在抽象系統中就會有一個影像壞路徑。如果抽象系統中所有路徑都是好的，則原始系統中所有路徑也都是好的。如果抽象系統中存在一條壞路徑，一條看似壞的路徑，你需要細化 (refine) 抽象。系統性的方法是 Ed 談到的 CGAR (Counterexample-Guided Abstraction Refinement) 技術。
緊湊表示 (Compact representations)，我想我們都知道 BDDs (Binary Decision Diagrams)。對於硬體設計，它們工作得很好。狀態空間對於軟體來說不一定那麼結構化。但最近的進展是 Ed 談到的基於 SAT 的有界模型檢驗 (SAT-based bounded model checking)。
組成性 (Compositionality)，分而治之，是一個很好的主意。讓它真正發揮作用存在問題。必須合成輔助斷言和輔助過程，類似於迴圈不變式。因此，在實踐中，到目前為止，它的影響不如我們預期的那樣大。
模型檢驗的實際應用
模型檢驗在實踐中適用於哪些系統？硬體、軟體、協定、嵌入式系統。還有非傳統應用，例如驗證 AI 中的代理系統、分析法律合約、系統生物學。應用領域包括硬體供應商、軟體開發商、政府機構、電子設計自動化、航空航太系統、汽車工程，以及包括 IBM、Intel 和 NASA 等各種組織，都使用模型檢驗。
早期反應與發展演進
現在讓我談談模型檢驗早期的反響。在 1980 年代早期，學術氛圍非常理論化。有一個稱為「程式邏輯」的社群，專注於用於推理程式的邏輯。這些邏輯為其自身而研究，有時也應用於驗證。其中關鍵的是模態和時態邏輯，例如 Fisher 和 Ladner 的命題動態邏輯 (propositional dynamic logic)，以及許多種類的時態邏輯。當時正在研究的關鍵問題是可滿足性 (satisfiability)。給定邏輯中的一個公式 F，它是否在某個解釋下為真？這是在為其自身而研究，但它的對偶是有效性 (validity)，這對於驗證具體程式可能有用。
模型檢驗涉及檢查一個公式 F 在一個給定的解釋下是否為真。當人們聽到這個時，產生了一些困惑。他們認為這是一種令人不安的新奇事物。它不是可滿足性，也不是有效性。那它是什麼？有一個評論說這令人困惑。另一個評論是，除非你能做到這樣或那樣，否則就省點樹木，別做這項工作了。總的來說，人們認為它永遠不會成功，狀態爆炸，即使沒有別的原因，也會讓你失敗。
好吧，後來我們得到了一些更好的評論。有一天晚上，Dijkstra 在我家，他說模型檢驗是一種可接受的拐杖。如果你不打算將程式的建構與其證明同步進行，那麼有模型檢驗總比沒有好。Amir Pnueli 在他的圖靈獎演講中，稱模型檢驗是該領域「工程化」(ingenierization) 的第一步。Daniel Jackson 說模型檢驗拯救了形式化方法聲譽。當我有幸見到 Saul Kripke 時，我告訴他我們用 Kripke 結構能做些什麼，他說：「我從沒想過那樣」，這我覺得有點令人耳目一新。
好的，那麼模型檢驗的進展或演變如何？我認為我們最初的框架是可行的。你有一個有用的邏輯和一些演算法的結合。它對於一些小型例子很有用，但你不能做任何大型的事情，所以顯然需要改進。
它能夠偵測臭蟲，這是證明理論方法通常做不到的，並且它將程式開發與驗證分開，我認為這有助於工業界的採納。Moore's Law 則給了我們更大、更快的電腦，因此我們吸引了起初數十名，然後數百名非常有才華的研究人員和使用者，這個領域也成長了。
好吧，它不能做到所有事情，這是這裡要說的。
成就與展望
模型檢驗取得了什麼成就？在實際層面上，再次強調，我們現在確實進行驗證了。二十七、二十八年前，我們只是談論它。從概念上講，有趣的是我們可以擺脫證明，省略證明，而只使用搜尋。而且它在大型學校的教育方面產生了一些影響。
現在，我想說模型檢驗在小部分上實現了 Leibniz 的夢想，即建立一個機械式的方案來計算真理。存在一種「通用文字」(lingua characteristica universalis)，一種所有知識都可以形式化表達的語言——時態邏輯；然後是一種「理性演算機」(calculus ratiocinator)，一種計算此類形式化斷言真值的方法——模型檢驗演算法。我的目標是努力讓模型檢驗實現更多 Leibniz 的夢想。