計算機輔助驗證 Computer Aided Verification 熊博安 國立中正大學 資訊工程研究所 〈部分投影片內容取自中央研究院資訊科學研究所王凡副研究員所開設之課程〉

Course Objectives Motivated Learning Formal System Modeling Formal Specification Model Checking Algorithms State-Space Reduction Techniques Applying Verification Tools to Real-World Systems and Protocols

規格指定、描述 v/s 驗證 規格指定（specification） : 行為描述（description）： 使用者對系統的要求 行為描述（description）： 使用者對系統行為的描述 與specification間，並無一定的區隔 驗證 （verification） : 系統設計有達到指定規格嗎？

正規指定、描述 vs 自動驗證 正規（formal）規格指定 : 自動（automatic）驗證 : 以數學的嚴謹語意表達規格指定 以電腦輔助（computer-aided）技術進行驗證

為什麼要研究正規描述方法？ 經由數學化的嚴謹定義，讓工程師、使用者更深入瞭解要設計的系統 減少自然語言的含混，減少溝通、討論、閱讀時的相互誤解 對系統的抽象精確描述 產生嚴謹的數學模型，以利正規驗證的分析

為什麼要研究自動驗證技術 ？ 系統設計愈趨複雜 解除大型系統設計之負擔 釋放人類的創造力 避免設計錯誤晚期修正的龐大成本 未來驗證技術的核心

Pentium Bug Floating Point Divide 應有十八位數準確性 只有四位數準確性 Pentium 60MHz、90MHz 範例： 5505001 / 294911 錯誤答案：18.66600093 正確答案：18.6665197

Pentium Bug （續） 只對特定數對（number pair）產生錯誤 重複發生。 影響大型科學、統計、工程計算、試算表、模擬、等應用。 由Pentium compile的軟體，都有可能受影響。

Pentium Bug （續） 由Lynchburg College的Dr. Thomas R. Nicely首度發現 nicely@acavax.lynchburg.edu Compuserve 網路，於 10/30/1994發佈 First in printed media on 11/7/1994 在1994年中，bug已經排除。但Intel在年底才對大客戶提供正確的晶片。要退貨，需個別處理，證明確實發生錯誤

Pentium Bug （續） 引發了formal verification研究的熱潮 目前Intel維持了一個龐大的formal method研究團隊。其規模與組織，為業務機密。 鹹魚翻身！ 許多研究經費流入。 適時的理論、實驗突破。

John R. Garman Deputy Chief Spacecraft Software Division THE "BUG" HEARD 'ROUND THE WORLD Discussion of the Software Problem Which Delayed the First Shuttle Orbital Flight John R. Garman Deputy Chief Spacecraft Software Division NASA, Johnson Space Center Houston, Texas Aug 24, 1981 ACM SIFSOFT Software Engineering Notes, Vol. 6, Nr. 5, Oct, 1981

4/10/1981, 太空梭預定第一次發射前二十分鐘，發現第五套備用電腦不能initialize THE "BUG" HEARD 'ROUND THE WORLD（續） Discussion of the Software Problem Which Delayed the First Shuttle Orbital Flight 4/10/1981, 太空梭預定第一次發射前二十分鐘，發現第五套備用電腦不能initialize 當時太空梭上，有四套General Purpose Computer（GPC）以及一套備用電腦。 以FO/FS為容錯設計要求 一套GPC出錯，仍能Vote；兩套錯，仍能安全返航

cyclic processing GPC與備用電腦上的程式系統，由不同人員發展。 THE "BUG" HEARD 'ROUND THE WORLD（續） Discussion of the Software Problem Which Delayed the First Shuttle Orbital Flight GPC與備用電腦上的程式系統，由不同人員發展。 cyclic processing GPC上的程式在預定發射前，已經跑了三十個小時，未嘗出錯。

GPC中有些processes已經out-of-phase了 備份電腦抓不到out-of-phase的資料，判斷GPC已經出錯。 THE "BUG" HEARD 'ROUND THE WORLD（續） Discussion of the Software Problem Which Delayed the First Shuttle Orbital Flight 在錯誤發生後一個小時，IBM將GPC中的memory dump出來，發現一個Software bug，timing synchrony出了錯誤。 GPC中有些processes已經out-of-phase了 備份電腦抓不到out-of-phase的資料，判斷GPC已經出錯。

複雜系統的軟體錯誤 特殊的事件順序下，激醒蟄伏中軟體錯誤。 傳統的test、simulation不能測出所有的事件順序。

複雜系統的軟體錯誤（續） 但電腦自動驗證的技術，在面對龐大的複雜度時，還是有不能盡力之時。 目前可求助於下列三者的整合： 良好的系統設計規範 模擬、測試，以檢驗明顯的錯誤 正規驗證（自動與手做），以證明系統設計的可靠性。

重要勢力分佈（美國） 模式檢驗 (Model Checking) 一階邏輯 (First-Order Logic) AT&T、CMU、UC-Berkeley、Stanford、North Carolina、Cornell、Intel、 Cadence-Berkeley 一階邏輯 (First-Order Logic) UT-Austin、SRI、MIT、MITRE、 XEROX-PARC

重要勢力分佈（歐洲） 處理代數 (Process Algebra) 正規方法 (Formal Methods) + Oxford、Cambridge、Edinburgh、Uppsala 正規方法 (Formal Methods) + Oxford、IFAD、IBM UK、CRI、Formal Systems Ltd、Praxis、CWI、VERIMAG

重要研討會（專屬） CAV (Computer-Aided Verification) FME (Formal Methods Europe) AMAST (Algebraic Methodo. & Sw Tech.) TACAS (Tools & Algorithms for CAS) TAPSOFT PROCOMET FORTE (Formal Description Technique)

重要研討會（含相關 session ) * FOCS * STOC * LICS * PODC * POPL * MFCS * STACS * RTSS * RTAS * ICALP * CONCUR * FORTE * SAS * CADE * FTRTFT * RTCSA

今日之理論： 指定表達能力 v/s 驗證複雜度 的平衡點 語言的表達能力 驗證問題複雜度 表達能力豐富 表達能力簡單 Undecidable nonelementary EXPSPACE EXPTIME PSPACE 驗證問題複雜度 NP PTIME

驗證複雜度的來源 ： 系統狀態的可能 ─ 天文數字 無限制的變數值範圍 非規則行為 ─ 不能用有限自動機描述的行為 每一個變數的值 程式執行的位址 各通訊通道的內容 無限制的變數值範圍 非規則行為 ─ 不能用有限自動機描述的行為 堆疊(stack)、排序(queue) 多項式運算、加減乘除 演繹法 （induction)

今日之理論 指定表達能力 vs 驗證複雜度的平衡點 非規則系統→證明檢驗 (proof checking) 規則行為系統 ★★★ 由工程師遵循經驗法則進行良好設計 由工程師導引自動驗證工具（十八般武藝） 規則行為系統 ★★★ 所需時間與記憶容量仍是驚人 高效能自動驗證演算法 控制計算時間、記憶容量

流派介紹 正規行為描述 自動驗證技術

流派介紹：正規行為描述 圖形語言：statechart、modechart 自動機理論（automaton theory） 派翠網路（Petri-Net） 一階邏輯（first-order logics） 時態邏輯（temporal logics） 傳統的正規程式語意 (formal semantics) 正規方法（formal methods） 處理代數（process algebra）

流派介紹：正規行為描述 自動機理論（automaton theory） 時態邏輯（temporal logics） 無時鐘的discrete 自動機 有時鐘的dense-time 自動機 混合式自動機（hybrid automata） 時態邏輯（temporal logics） 無時鐘的時態邏輯 真時時態邏輯

Timed Automata (for Real-Time Systems) 監控 命中 50ms 修正

Timed Automata (for Real-Time Systems) 在500ms的限期內，每50ms監測敵蹤並修正飛彈方向，直到命中目標為止 x:=0; z:=0 x、 z 是實數值系統時鐘。 監控 x、z在系統開始時，被設為零。 x<500ms z50ms 命中 z=50ms z在每次監控週期，被設為零。 z:=0; 修正

正規行為描述 : Petri-Net 1972 年，C.A. Petri places : 有限數個 tokens : transitions enabled : 如果每個 來源place中，都有token firing: enabled transition 自 來源places中，各取一token； 在目的places中，各放一個token。

正規行為描述 : Petri-Net (2,1,0) 實質上同於Karp、Miller 的向量加法系統 不能檢驗事件的不存在 狀態（state） marking : places à N (2,1,0)

正規行為描述 : Petri-Net computation : （state sequence） a b b a b a 由enabled transitions 串接起來的 marking sequence interleaving semantics a b b a b a (2,1,0)→(1,0,1)→(2,1,0)→(1,0,1)→………

Petri-Net： 驗證問題 經由一個initial marking，可以走到無限個marking Reachability 問題： 給定兩個marking M1、M2,是否有一個computation ，可以從M1走到M2? Reachability 問題有解，但不知複雜度。

正規行為描述 : 圖形語言 Statecharts David Harel, 1986 由自動機理論擴展出來 可以描述並行計算、離散事件系統 science of computer programming 由自動機理論擴展出來 可以描述並行計算、離散事件系統 nested modules

正規行為描述 : Statechart Parallel modes for orthogonality avionic system general mode radar abc-system cruise off off lever-on switch-on navigate touchdown switch-off standby lever-off calibration end-calibration on-ground take off on end-warmup on

正規行為描述 : Statechart display H wait update date time a a a a a 2min. in time display wait c H d update date c’ d time b 2min. in date a a a a a stopwatch chime alarm 2 alarm 1 off H off H off H d d d d d d on on on c c b b update 2 update 1

正規行為描述 :圖形語言 Modechart F. Jahanian, A.K. Mok, 1986 IEEE Transactions on SE statechart的real-time擴充 semantics 由 RTL 定義。 RTL（real-time logic）也是由Jahanian和Mok提出的。（IEEE TC）

正規行為描述 : Modechart Rail-road Crossing Control System Gate-controller Monitor ↑approach [0, ∞) up lower far approach ↑approach [100, 100] [100, 100] [20, 100] [20, 50] raise down passed crossing ↑passed [0, ∞)

正規行為描述：時態邏輯 由modal logics 的一支，發展出來。 在時態邏輯中， 討論possible world的動態結構 兩個運算元：□、◇ □ ：所有的possible world，命題皆成立 ◇ ：存在一個possible world，命題成立 modal logics 的模型為Kripke structure(directed graph) 在時態邏輯中， □ ：自今而後，命題永遠成立 ◇ ：將來有一刻，命題成立

正規行為描述：時態邏輯 線性結構（linear-time）的模型（model） 樹狀結構的模型 （branching-time） s1 s2 sk s0 s0 s2 s1 s5 s4 s3 $ ： 存在一個path "： 對所有path

★Amir Pnueli, 1996 Turing Award Winner 正規行為描述：時態邏輯 線性結構（linear-time） 與PLTL（Propositional Linear Temporal Logic） 遲早有一刻，process p 會被執行。 ◇p：liveness property Øp p ★Amir Pnueli, 1996 Turing Award Winner

正規行為描述：時態邏輯 線性結構（linear-time） 與PLTL（Propositional Linear Temporal Logic） Process p 和 q 永遠不會同時在執行狀態 □ Ø (p Ù q） : safety property p q

正規行為描述：時態邏輯 線性結構（linear-time） 與PLTL（Propositional Linear Temporal Logic） p一直被滿足，直到q被滿足。(p until q) p U q 滿足 p p p p q 滿足 p p p p Ù q q 不滿足 p p p q

正規驗證：線性時態邏輯 滿足（satisfaction） 的關係 一個線性時態邏輯公式定義一個模型集合。 一個線性結構滿足一個線性時態邏輯公式 一個線性時態邏輯公式定義一個模型集合。 一個邏輯公式是unsatisfiable如果他的模型集合是空集合。 測驗 P Ù Ø S 的 unsatisfiability P 是系統行為描述 S 是specification PLTL的satisfiability問題是PSPACE-complete

正規行為描述：時態邏輯 樹狀結構（branching-time）與 CTL（Computation Tree Logic） Inevitability Øp p Øp p p

正規行為描述：時態邏輯 樹狀結構（branching-time） 與CTL（Computation Tree Logic） $ ØpU p Øp Øp Øp Øp Øp p Reachability

正規驗證：樹狀時態邏輯 滿足（satisfaction） 的關係 一個樹狀時態邏輯公式定義一個模型集合。 一個樹狀結構滿足一個樹狀時態邏輯公式 一個樹狀時態邏輯公式定義一個模型集合。 一個邏輯公式是unsatisfiable如果他的模型集合是空集合。 測驗P Ù Ø S的unsatisfiability CTL 的satisfiability問題是deterministic EXPTIME-complete

模型檢驗（model-checking） 給定一個模型 M，和一個時態邏輯公式 P，請問 M 滿足P 嗎？ 通常M以有限自動機表達。 在CTL的情況下，模型檢驗可在PTIME內解決。

模型檢驗（model-checking） 狀態空間分析 狀態空間表示法：有向圖 節點：系統狀態 箭頭：狀態轉換 規則系統行為 有限但極大(天文數字)之狀態空間 執行 完成 等待

一個全加器的邏輯公式 Øx x Øy y ØC C S = x ⊕ y ⊕ C

operational semantics denotational semantics axiomatic semantics 流派介紹：傳統的正規語意 operational semantics 定義抽象電腦 denotational semantics 將程式視為函數 (denotation) axiomatic semantics pre-condition與post-conditions 可以和正規驗證技術掛勾

正規驗證技術： Axiomatic Semantics sequential programs E. W. Dijkstra, Turing Award A Discipline of Programming, Prentice-Hall, 1976 distributed programs Chandy、Misra 的 UNITY Parallel Program Design - A Foundation Addison-Wesley, 1988

正規驗證技術： Axiomatic Semantics guarded-command language x, y := x + y, 0 if y>0 Fairness assumption, interleaving semantics program composition precondition、postcondition {y>0} x,y:= x+y,0 if y>0 {y=0} proof-checking 許多laws safety properties、liveness properties

流派介紹：自動驗證技術 證明檢驗 （proof-checking） automatic verification resolution-based prover Floyd-Hoare Logics : axiomatic prover proof paradigm : VDM automatic verification 模型檢驗（model-checking） language inclusion bi-simulation

實際工業運用上之成就 （I） 一階邏輯（first-order logic) Boyer & Moore 的 NqThm 證明檢驗 1985 年，驗證四位元 FM 8501 CPU 至位元層次。 高階語言編譯程式（compiler) 參考書：A Computational Logic Handbook, Academic Press, 1988

實際工業運用上之成就 （II） 正規方法（formal method) OCCAM IMS T800 transputer 研發時間估計節省十二個月 1990 年英國女王獎！！！ （49 位獲獎）

實際工業運用上之成就 （III） 正規方法（formal method) Z notations 的正規描述方法 IMS CICS 研發經費估計節省5百餘萬元 1992 年英國女王獎！！！

實際工業運用上之成就 （IV） 模式檢驗 （model-checking) Burch, Clarke, McMillan, Dill, Hwang 二元決定圖（BDD）符號處理 CMU 的 SMV 系統， 全自動 Intel 32位元ALU，8 個暫存器，兩層 pipeline 狀態空間數目達 10120 在SUN 4 上 4 時 20 分。

實際工業運用上之成就 （V） Symbolic Trajectory Evaluation Hazelburst, Seger 64 位元乘法器 簡單的、或 Wallace tree 硬體驗證（no memory） 在Sparc 10/51 上 800 秒。

實際工業運用上之成就 （VI） 一階邏輯與混合式自動機 Bosscher, Polak, Vaandrager 證明檢驗 Phillip 音響控制網路實體層 考慮信號電壓的變化、晶體頻率的穩定性 不考慮匯流排擠撞 (collison)、信號延誤 證明1/17 頻率誤差可接受。 （Phillip 以 5% 為設計標準） 後經Henzinger 的 HyTech 自動驗證完成。

二元決定圖 : BDD （Binary Decision Diagram） 邏輯公式的最小標準型（normal form) 最小 ： 高效率 相對於特定變數評估順序 標準型 ： 同值的公式有 唯一的表示法 x 1 y z 1 1 (x Ú Øy) Ù z 1 1

(x Ú Øy) Ù z 變數評估順序對BDD的size影響 xßzßy xßyßz x x 1 1 z z z y y 1 z 1 1 1 x xßyßz 1 1 z z z y y 1 z 1 1 1 1 1 1

BDD:邏輯函數的最小標準型 xÙ(yÚØy)Ùz x x 1 1 y 1 z z 1 1 1 1 正確的BDD 非 BDD

Even Parity 的 BDD (ØxÙØyÙØzÙØw) Ú (ØxÙØyÙzÙw) Ú (ØxÙyÙØzÙw) 1 y y (ØxÙØyÙØzÙØw) Ú (ØxÙØyÙzÙw) Ú (ØxÙyÙØzÙw) Ú (ØxÙyÙzÙØw) Ú (xÙØyÙØzÙw) Ú (xÙØyÙzÙØw) Ú (xÙyÙØzÙØw) Ú (xÙyÙzÙw) 1 1 z z 1 1 w w 1 1 1 O (n 2 n-1) O (2n+1) disjunctive normal form

BDD 的邏輯運算 Ø B1 給定兩個BDD ：B1、B2，下列邏輯函數之BDD，皆有高效率演算法，可以計算。 B1 Ú B2