很高興能在 Embedded Systems Week 演講，我特別感謝 Embedded Systems Week 指導委員會促成此事。我也想熱烈感謝 Amir Pnueli 的介紹。今天我將從更廣泛的角度來談談驗證的未來，這是我的個人觀點。首先，我想說達成正確性有兩種不同的方式：一種是檢查系統或系統的模型是否符合既定的需求；另一種是透過工程師和系統建構者通常使用的建構性成果，例如演算法、協定、架構。因此，當你使用一個已被證明是正確的架構時，你就免費獲得了正確性。舉例來說，如果你使用時間票據架構（time-ticket architecture）並正確實作這個架構，那麼你就擁有了一個即時容錯系統。我想說的是，電腦科學與更成熟的學科（即基於物理學的學科）之間的一個重大區別在於，對於電腦科學來說，事後驗證非常重要，而其他學科則允許建構性和可預測性。
檢查正確性
在這張投影片中，我想說檢查正確性有不同的方法。你可以透過觀察其行為、透過測試來檢查實體原型（physical prototype）的正確性，或者你可以在模型（即虛擬軟體原型）上檢查正確性。在這方面，你又有兩種選擇。你可以使用特設模型（ad hoc models），或者使用形式化模型（formal models）。兩者的重大區別在於形式化模型具有明確定義的狀態（state）和轉換（transition）概念，並且驗證是應用於形式化模型的，這使得窮盡性（exhaustivity）成為可能。在我的演講中，我將主要關注演算法驗證（algorithmic verification），特別是模型檢查（model checking），但我要說的內容在某種程度上也適用於演繹驗證（deductive verification）。因此，對於驗證，你需要三個基本要素。你需要描述系統行為的需求（requirements），這是所有潛在用戶期望的行為，以一組性質（properties）的形式表達。你需要模型（models），這些是可執行的模型，描述系統行為作為其狀態上的轉換關係。最後，你需要驗證方法來比較模型與需求。
需求規格說明
現在，快速回顧一下我們在這三個要素方面的現狀。關於需求規格說明（requirements specification），我想說今天有兩種風格來表達需求。基於狀態的（State-based），你在其中使用機器來指定系統的可觀察行為，這裡我給了一個自動機，它指定了一個特定抽象層級的協定，即發送（send）和接收（receive）的交替。你也可以使用另一種選擇，即使用公式，特別是時序邏輯（temporal logic），這在之前已經解釋過了。因此，對於這個特定的協定，你可以說，例如，總是不可避免地啟用發送（enable send），並且總是不可避免地啟用接收（enable receive）。我希望你理解這兩個公式並不能精確地指定這個行為。你需要使用直到（until）運算符才能精確地描述這個行為。人們普遍認為，基於狀態的規格說明很適合描述事件之間的因果關係，也就是動作序列。而基於性質的規格說明很適合表達全域性質（global properties），例如互斥性（mutual exclusion）、終止性（termination）和公平性（fairness）。我想在這裡適當地說幾句關於時序邏輯的話，它確實是理解並形式化併發系統需求的一個突破。但是，我想說的是，使用時序邏輯存在一些問題。它們的使用不是微不足道的。為什麼？因為即使是表達非常常見的概念，其表述上也存在一些細微的差異。例如，如果你考慮公式「always inevitable F」，你直觀上理解它是什麼意思，但它對於線性時間（linear time）和分支時間（branching time）時序邏輯卻有不同的含義。使用時序邏輯的另一個問題是規格說明的性質是合取的（conjunctive），因此一個規格說明的含義是該規格說明中所有公式含義的交集，而這個交集可能是空的，這意味著你的規格說明是不健全的（not sound）。但更嚴重的問題是如何檢查規格說明的完備性（completeness），這表徵了你的規格說明的嚴謹程度。因此，在實踐中，你需要結合基於性質和基於狀態的風格。一個已經提到的例子是 PSL，這是一種由工業界和研究人員組成的聯盟為規格說明電路而開發的語言。但我認為這種語言並不是真正成功的。今天，需求規格說明的一個重要趨勢是我們正在轉向基於狀態的規格說明。在實踐中，我們傾向於使用基於狀態的規格說明的語義變體。例如，工程師使用的一個有趣的例子是訊息序列圖（message sequence charts），這是 UML 的需求表達語言，你可以在其中指定進程之間的互動。進程是垂直線，互動是水平線。這樣做可以區分必須（must）和可能（may）的互動，這使得表達某些局部活性（local liveness）成為可能。在我看來，需求規格說明語言的狀態在表達功能性質方面是令人滿意的，但在表達許多應用領域的非功能性需求（extra-functional requirements）方面還有很多工作要做。例如，對於安全性，如何表達隱私性質？例如，對於可重構性，如何表達功能之間的不干擾性？服務品質（quality of service）等等。
建構模型
現在來談談建構模型。顯然，模型應該是忠實的（faithful），也就是說，我們為模型驗證的任何性質都應該在實際系統中成立，並且模型應該從系統描述中自動生成。這對於避免錯誤非常重要。因此，對於硬體，如果你從 RTL 層級的描述開始，例如，很容易獲得邏輯有限狀態模型，表示為布林方程組。這是微不足道的，我認為這解釋了模型檢查在硬體驗證中的成功。現在對於軟體驗證，問題要困難得多。如果你從用 Java 或 C 等真實語言編寫的程式開始，那麼如果你想驗證這些程式，首先要定義它們的含義，為此你必須定義操作語義（operational semantics），最終解決這些語言可能存在的某些語義歧義（semantic ambiguities），這是一項非微不足道的任務。一旦你定義了語義，即操作語義，這就定義了程式的含義，然後你必須進行一些簡化，進行一些抽象化（abstractions）。例如，這裡我使用一個布林變數 B 來區分 X 的正負，這個過程應該自動完成。有一些工具成功地做到了這一點，但這裡仍然有很多工作要做。最後，如果你想為軟硬體混合系統建構模型，這對於嵌入式系統的驗證非常重要，我認為今天沒有忠實的建模技術來處理混合系統，僅僅是因為我們不了解軟體如何與底層執行平台互動。今天，即使對於非常簡單的系統，例如感測器網路的節點，大多數針對混合系統的驗證工作都是透過測試完成的。所以理想情況下，我希望有現代技術可以從應用軟體開始，建構一個模型，然後我有一個執行平台的模型，接著我有一種方法來組合這兩個模型，而今天我不知道如何做到這一點，我認為這將一直是一個開放性問題，只要我們不了解作業系統和中介軟體究竟是如何運作的。
演算法驗證與抽象化
最後，在這次概述中，我想簡單談談演算法驗證，特別是使用抽象化的重要性。這個想法之前已經解釋過了。如果你想驗證系統 S 是否符合性質 F，那麼驗證某個抽象系統 SA 是否滿足性質 FA 就足夠了，並且抽象系統比具體系統更簡單。這對於某些類型的性質是可行的，我想在這裡承認 CUSO 的工作對我的影響。在 80 年代初期，我們一直在合作，我們的辦公室在同一走廊，所以我也受到了他們的想法的影響。CUSO 提出了一個框架，一個用於計算抽象化的通用框架。我不會在這裡提供詳細資訊，但這個想法非常簡單，非常優雅，核心思想是透過一對單調函數（monotic functions），即抽象化函數 alpha 和具體化函數 gamma，將左邊的具體性質的格（lattice）與右邊的抽象性質的格關聯起來。因此，這個想法是，正如你可能知道的，任何驗證問題都可以歸結為不動點計算（fixed point computation）問題，即將函數 f 的不動點計算約化為 f 的最佳近似（best approximation）。因此，理論允許計算健全且嚴謹的函數近似。我想在這裡提倡兩個領域之間的匯聚，即模型檢查和抽象解釋（abstract interpretation）這兩個領域，它們在過去 20 多年來平行發展，互動不多。我認為這兩個領域之間存在非常有趣的互補性。我可能不會詳細解釋這一點。模型檢查始於驗證有限狀態系統，然後我們使用抽象化來解決無限狀態系統的驗證問題，而抽象解釋則局限於透過兩個可讀性分析進行計算。我認為，透過使用抽象解釋社群開發的抽象領域（abstract domains）庫，模型檢查仍然可以獲得重要的成果。
未來工作方向
這結束了我的概述，接下來我想提出幾個工作方向，當然這些方向也反映了我個人過去至少五年來的研究方向。一個重要的問題是基於元件的建模（component-based modeling）。為什麼選擇基於元件的建模？為了能夠將異質元件組合起來，建構軟硬體混合系統的忠實模型。我希望這個社群能夠理解這一點，所以想法是能夠透過一致地組合異質元件來建構複雜系統。這是我們今天還不知道如何做到的。異質性至少有三個深層來源，這是我們與 Tom Hensinger 在一篇共同論文中區分的。有些元件是同步的（synchronous），有些是非同步的（asynchronous），你有許多不同的互動機制，許多不同的抽象層級。我想在這裡說，我們開發的大多數組合理論都基於低層級的基於自動機的組合，我希望有一個統一的組成典範（unified composition paradigm），其中包含架構約束。我想知道如果我有一些元件，並且我使用協定、排程器、匯流排來組合它們，結果會是什麼。
下一個工作方向與上一個相關，是組合式驗證（compositional verification）。這個想法之前已經解釋過了，非常簡單，就是如何從個別元件及其架構的性質來證明組合元件的全域性質？如果我有一些微笑的元件，是否有理論可以得到一個全域微笑的系統？組合式驗證在過去 15 年是一個非常活躍的研究領域，但沒有取得顯著成果，但我認為組合性是必須的，如果我們想戰勝複雜性，我們必須採取分而治之（divide and conquer）的方法。
那麼，方向是什麼？我這裡建議的是從基於自動機的組成操作轉向... 到目前為止，我們一直在嘗試開發通用理論來組合地證明安全性質（safety properties）甚至活性性質（liveness properties），而我想研究更普遍的組合操作方法。為什麼？因為如果你有基於元件的組合操作，可能會出現一些當你使用低層級組合時隱藏起來的性質，對於特定性質，例如無死鎖性（deadlock freedom）、互斥性，即使無死鎖性和互斥性都是安全性質，我認為你不應該完全使用相同的技術。
所以我這裡建議的是，我們應該透過在兩個方向努力來開發組合性成果。首先，針對特定類型的系統、特定架構、特定程式設計模型、特定執行模型，以及針對特定類型的性質，如無死鎖性、互斥性和及時性（timeliness）來開發組合性成果。例如，針對資料流系統中的無死鎖性或主從式架構（client servers architectures）中的互斥性獲得特定結果是很重要的。我認為當我們這樣做時，我們就會擁有... 所以這個組合性理論以及這些理論的組合將導致可驗證性條件（verifiability conditions），也就是在這些條件下，特定性質的驗證變得更容易，當然也會導致透過建構在某種程度上是正確的系統類別，因為如果我知道如何以低成本輕鬆驗證一個性質，那麼我就獲得了一個透過建構達成正確性的結果。
為了說明這個想法，我想談談我們在 Verimag 正在進行的研究，這是一項進行中的工作，關於組合性，我們有一個名為 BIP 的元件框架，對於這個框架中的元件，我們希望開發理論，我們已經開發了理論，用於檢查由無死鎖元件建構的系統的全域無死鎖性，透過分別分析元件和架構。因此，如果我例如有這兩個元件並且它們是無死鎖的，直線是一個連接器，它表示它們可以透過會合（rendezvous）互動，P1 和 P2 是埠（ports），很容易看出如果每個元件都是無死鎖的，這意味著如果它阻塞，那麼它正在透過某個埠尋求互動，很容易看出如果兩者都是無死鎖的，那麼系統是全域無死鎖的。
如果我現在取相同的元件，但有兩個連接器，因此有兩種互動的可能性，這裡存在死鎖的可能性，為什麼會存在死鎖的可能性？因為一個元件可能正在透過 P1 尋求互動，而另一個元件正在透過 Q2 尋求互動，你可以看到，如果連接器圖中存在循環，這些循環可能會引入死鎖，這種死鎖我們可以透過像這樣的謂詞（predicate）來描述，它表示啟用 P1 但未啟用 P2，並且啟用 Q2 但未啟用 Q1。這是一個我們可以透過分析元件的程式碼和架構來提取的謂詞，當然，如果你有像這樣的循環，你可以找到潛在的死鎖。一旦你知道了透過分析架構發現的潛在死鎖，你就可以應用一些技術來查看這些潛在死鎖是否可行，我們正在這樣做，我們有一個工具來做這件事，這個技術非常簡單，我們將死鎖與不變數（invariants）進行合取，不變數是對系統可達狀態（reachable states）集合的過度近似（over approximations），這些不變數我們是組合地計算的，我沒有時間提供詳細資訊，但我認為我們取得了非常好的成果，我們有一些啟發式方法（heuristics），我們有一個工具來做這件事。好的，現在也許是時候總結了。
結論
總結一下，我想說的是，事後驗證當然不是保證正確性的唯一方法，我認為有時候我們研究人員、研究社群可能過於雄心勃勃或過於普遍化了，我認為相比之下，系統工程師使用的解決方案是基於在技術上已被證明是穩固、有趣等的架構和結構。所以這裡的想法是我們應該將重點限制在特定類型的系統上，這就是想法。所以訊息是我們應該專注於操作上相關且技術上成功的系統子類別和性質的組合式建模和驗證。我認為透過這樣做，這是一個現實的方法，而且我認為這也將有助於使電腦科學成為一個更成熟的學科，透過彌合形式方法和驗證與其他更具建構性的知識體系（演算法和複雜性）之間的差距，這也將是一個有趣的成就。謝謝大家的聆聽。好的，我想我們還有時間回答幾個問題，所以如果大家有任何問題或評論，請儘管提出，並請將問題直接提給特定的演講者。
問答環節
好的，到目前為止我有一個問題要問 Joseph。好的，也許我們可以跳過這個問題。我現在有麥克風了。所有的問題... 看起來組合式驗證可能不適用於所有系統，有些系統可能耦合得非常緊密，以至於你無法以可以用組合式推理（compositional reasoning）的方式對它們進行分割。你知道衡量兩個進程、兩個元件之間耦合程度的好方法嗎？
這確實是一個非常有趣的問題。好的，我對此有一些直覺和想法，但... 好吧，一個想法是嘗試分析我們所謂的互動圖（interaction graph）或依賴圖（dependency graph），因為在某些情況下，例如如果互動圖中沒有循環，那麼證明無死鎖性是微不足道的；如果元件是無死鎖的，那麼如果沒有循環，系統就是無死鎖的。所以我認為結構的複雜性，即架構的結構、互動的結構，肯定是非常重要的，當然，如果它非常複雜，那麼找到組合性結果就會更困難。好的，這裡有一個問題。
如果我能再追問一個問題，Paul，你談到了驗證軟體系統的困難，我們也期待資訊物理系統（cyber physical systems），它們與物理系統相關。你認為驗證系統有多少解決方案會來自數學，即更好的證明技術， versus 架構方法，也就是限制我們允許建構的系統類型？
這是一個有趣的問題。我最近花了很多時間試圖學習混合系統（hybrid systems）以及如何驗證混合自主系統，也許除了早期的評論之外，我們還會有後續的評論。符號模型檢查（symbolic model checking）的重大進展在於我們使用 BDD 工具作為問題的判定程序（decision procedure），SAT 解算器（SAT solvers）也是如此，現在還有 SMT 解算器（SMT solvers），但我們目前對於非線性算術（non-linear arithmetic）沒有好的解算器。因此，像基於實代數閉域（real close fields）的柱狀代數分解（cylindrical algebraic decomposition）方向的一些進展，可能真的能在混合系統驗證方面實現突破。但在軟體方面，我認為這可能是一個完全不同的問題，在我看來，這是處理指標資料結構（pointer data structures）的問題，而且我認為數學對軟體驗證的幫助不會像對解決混合系統中非線性算術問題那樣大。
是的，作為補充回答，我認為在系統驗證中的問題在於軟體如何與平台互動，而在這裡，我認為也許架構解決方案至少可以是一個部分答案，特別是一些即時性質（real-time properties），你可能試圖在一個帶有時間資訊註釋的模型上驗證這些性質，問題在於你如何透過實作來保留這些性質，而要做到這一點，你必須對平台有非常好的了解，而今天關鍵問題是我們沒有平台的模型，今天我們甚至不了解例如作業系統如何與平台互動。好的，或者我們沒有作業系統的模型，而且我們沒有一個由軟體和硬體或中介軟體組成的系統的完整模型。
讓我再補充 Joseph 所說的。
總體而言，像 Windows 作業系統中的軟體，指標的使用非常普遍。然而，在不同類型的嵌入式軟體中，我認為情況可能不同，而且動態分配指標資料結構可能不會被如此頻繁地使用，以保證某些最糟執行時間（worst-case execution time）的平衡。這種類型的嵌入式軟體可能就是繼硬體之後下一個值得挑戰的領域。因此，我認為可以在這類軟體上取得進展。
好的，我想我們現在還有另一個問題。
Eric Altman 來自 IBM。你怎麼知道大型規格本身是正確的，是否存在類似哥德爾不完備定理（Gödel's incompleteness theorem）的問題，即如何知道規格在內部是正確且一致的？
嗯，你可以... 你的規格邏輯應該是可判定的（decidable），命題超時序邏輯（propositional super temporal logic），你可以透過檢查其可滿足性（satisfiability）來檢查它是否一致。但還有一個更深層的問題。存在驗證問題，即給定一個程式碼文字（program text），給定規格的文字字串（text string of the specification），它們各自有語義。這是一個數學問題。程式是否滿足規格？這就是我們解決的問題。你所說的是 Dijkstra 曾經稱之為愉快性問題（pleasantness problem）。我怎麼知道這段邏輯是否準確捕捉了我直觀上想要的東西？
這本質上是一個前形式化（pre-formal）的問題。你知道，我的意思是，你直觀上想要的東西，我的意思是，它在你腦袋裡是模糊不清的，或者更糟，也許是一個委員會想出來的，並用一些散文來描述它。我認為最好的方法可能是實際採取經驗方法，並模擬你的規格，試運行看看，看看你能否從中獲得一系列合理的行為。
我有一個務實的答案，來自多年處理真實範例的經驗。我相信你問題的答案是模型檢查與之前方法（即之前使用的邏輯）的一個重大區別所在。根據我們的經驗，我們花一半時間對規格進行除錯，另一半時間證明電路或協定是正確的。我們對此並不感到抱歉。而讓我們知道規格不好的一個原因在於我們得到了反例（counterexamples）。我們可以查看一個反例，然後常常會說，這個反例太荒謬了。我的規格肯定有問題。
所以我認為答案，你問題的真正答案在於模型檢查能產生反例，你可以利用這些反例來查看規格本身是否有誤。而且我認為如果你的規格不好，你無需感到抱歉。這是預料之中的，你會這樣做。
謝謝。
好的，我想我們時間到了，所以我建議如果大家還有其他問題，那麼請大家在休息時間抓住我們的三位得獎者，他們都參與了這次會議。請大家和我一起向他們三人表示感謝，感謝他們帶來了一系列富有資訊且具啟發性的圖靈獎演講。