近十年以來，計算機科學研究的進步大大推動了需求和設計驗證工具和技術的發展，其中最成功的技術當屬模型校驗。模型驗證與規范化建模語言的緊密結合，極大地推動了驗證自動化的發展。本文介紹了模型校驗的原理及工作方式。 模型校驗是最成功的需求驗證工具。模型校驗的基本原理如圖1所示。模型校驗工具的輸入是系統需求或設計（稱為模型）以及最終系統期望實現的特性（稱為“規范”）。如果給定的模型滿足給定的規范，那么工具將輸出yes，否則將生成反例。反例詳細描述了模型無法滿足規范的原因，通過研究反例，可以精確地定位模型的缺陷，如此反復。該方法的原理是通過確保模型滿足足夠多的系統特性以增強我們對模型正確性的信心。系統需求之所以稱為模型，因為這些模型表征的是需求或設計。 那么，哪種規范化語言可以用來定義模型呢？答案當然不是唯一的，因為不同應用領域的需求（或設計）差異很大。例如，銀行系統和空間系統在系統規模、結構、復雜度、系統數據的屬性及執行操作上的需求差異就很明顯。相反，大多數實時嵌入式或安全臨界系統都面向控制，而不是數據，這意味著這些系統的動態特性遠比業務邏輯（由系統維護的內部數據的結構及操作）重要。這些基于控制的系統可以應用于諸多領域：航天系統、航空電子、汽車系統、生物醫學儀器、工業自動化及過程控制、鐵路、核電站等。甚至數字硬件系統的通信和安全協議均可視為面向控制的系統。圖1：模型校驗方法。 對于面向控制的系統，可以采用有限狀態機（FSM）定義需求和設計，這是一種得到廣泛認可的抽象表示方法。當然，光靠FSM并不能對復雜的實際工業系統進行建模。我們還需要：1. 能將需求模塊化并區分需求等級；2. 能合并各組成部分的需求（或設計）；3. 能通過更新預先規定的變量和設備，防止可能出現的異常。 校驗設計需求時，通常可以通過回答一些問題得到結果。下面給出了校驗需求時最常問的一些問題： ＊ 設計需求是否準確地反映了用戶需求？需求中的每一事項是否與用戶的期望一致？需求是否包含用戶所要求的全部內容？ ＊ 設計需求是否表述清晰并無異義？是否能被用戶很好地理解？ ＊ 設計需求是否具有靈活性和可實現性？例如設計需求是否模塊化并具有良好的架構，從而有助于設計和開發？ ＊ 設計需求是否能輕松地定義驗收測試示例以驗證設計實現與需求的一致性。 ＊ 設計需求是否只是概要地描述而與具體的設計、實現及技術平臺等無關，從而使得設計人員和開發人員具有充分的自由度實現這些需求？ 回答這些問題當然絕非輕而易舉而且也沒有任何捷徑可循，但如果需求成功地超越了這些條條框框，那么無疑為優良系統的設計打下了堅實基礎。盡管可以利用類似UML這樣的建模工具，但仍然需要確保設計需求的質量。這個過程需要投入大量精力和時間，包括各種形式的審查，有時甚至還需要進行部分原型設計。此外，需求設計中采用多種表示方法（如UML中的表示方法）通常又將引發其他的問題,例如: ＊ 設計需求需要使用哪種表示方法？ ＊ 如何確保不同表示方法的描述的一致性？ 設計需求缺陷的成本通常很高，至少需要重設計并進行維護。錯誤的需求導致錯誤的系統行為并顯著增加成本，如喪失產品的時效性和本質特征，而對于工作在實時環境下的嵌入式安全臨界系統更是如此。為確保系統設計的質量，也需要考慮類似的問題。 改進需求和設計的一條途徑是利用自動化工具對需求和設計各環節的質量進行校驗。那么，哪種工具最適用呢？一般而言，校驗用英文描述的需求或設計極為困難。因此，必須采用一種清晰嚴格且無二義的規范化語言對需求進行描述。如果這種描述需求和設計的語言具有明確的語義，那么完全可以開發出自動化工具以分析這種語言描述的設計需求。這種采用嚴格語言描述需求或設計的基本思想已成為系統驗證的基石。 簡單的系統模型實例 首先，讓我們考察一下如何利用模型校驗工具驗證簡單的嵌入式系統特性。為此，我們采用Carnegie-Mellon大學開發的符號模型驗證器（symbolic model verifier,SMV）作為模型校驗工具。當然，我們也可以采用其他的模型校驗工具描述該模型。文章結束部分列出了可選的模型校驗工具及獲取方式。 如圖2所示，一個簡單的泵控系統通過泵P將源水槽A中的水傳送至接收水槽B。每個水槽都具有兩級刻度線：一個用來檢測水位是否為空（Empty），而另一個用來檢測水位是否已滿（Full）。如果水槽的水位既不為空也不為滿，那么水槽刻度線設定為ok；換言之，即水位高于空刻度線但低于滿刻度線。 最初，兩個水槽均為空。一旦水槽A的水位值為ok（從空開始），啟動泵并假定水槽B尚未為滿。只要水槽A不為空且水槽B不為滿，泵將持續工作。一旦水槽A為空或水槽B為滿，泵將停止工作。一旦泵啟動（或停止），系統將不會嘗試停止（或啟動）泵。雖然這個示例非常簡單，但可以很容易地擴展為控制多個源水槽和接收水槽的復雜泵管線網絡控制器，如應用在水處理系統或化工廠中的控制器。 表1：SMV模型描述和需求清單。 MODULE main VAR level_a : ｛Empty, ok, Full｝; —— lower tank level_b : ｛Empty, ok, Full｝; —— upper tank pump : ｛on, off｝; ASSIGN next（level_a） := case level_a = Empty : ｛Empty, ok｝; level_a = ok & pump = off : ｛ok, Full｝; level_a = ok & pump = on : ｛ok, Empty, Full｝; level_a = Full & pump = off : Full; level_a = Full & pump = on : ｛ok, Full｝; 1 : ｛ok, Empty, Full｝; esac; next（level_b） := case level_b = Empty & pump = off : Empty; level_b = Empty & pump = on : ｛Empty, ok｝; level_b = ok & pump = off : ｛ok, Empty｝; level_b = ok & pump = on : ｛ok, Empty, Full｝; level_b = Full & pump = off : ｛ok, Full｝; level_b = Full & pump = on : ｛ok, Full｝; 1 : ｛ok, Empty, Full｝; esac; next（pump） := case pump = off & （level_a = ok | level_a = Full） & （level_b = Empty | level_b = ok） : on; pump = on & （level_a = Empty | level_b = Full） : off; 1 : pump; —— keep pump status as it is esac; INIT （pump = off） SPEC —— pump if always off if ground tank is Empty or up tank is Full —— AG AF （pump = off -> （level_a = Empty | level_b = Full）） —— it is always possible to reach a state when the up tank is ok or Full AG （EF （level_b = ok | level_b = Full）） 系統狀態就可用上述3個變量的不同取值來表示。例如（level_a=Empty, level_b=ok, pump=off）和l （level_a=Empty, level_b=Full, pump=on）就可以表示系統狀態。在靠近結尾的INIT部分，定義了這些變量的初始值（這里，最初假定pump的初始值為off，而其他兩個變量則可取任意值）。 ASSIGN部分定義了系統如何從一個狀態遷移到另一個狀態。每個next語句都規定了特定變量的取值變化。所有這些賦值語句都假定可以并行執行；next語句定義為在該部分執行所有賦值語句后的最終結果。下層水槽的狀態可以從Empty狀態遷移到Empty或ok狀態；從ok狀態遷移到Empty或Full狀態，或保持為ok狀態（如果pump的狀態為on）；從ok狀態遷移到ok或Full狀態（如果pump的狀態為off）；如果pump狀態為off，那么下層水槽在Full狀態無法發生狀態遷移；如果泵狀態為on，則可遷移到ok或Full狀態。上層水槽也可規定類似的操作。 在系統內部，大多數模型校驗工具通常會將輸入模型擴展為具有Kripke結構的動態系統。擴展過程包括在EFSM中除去分層結構、并行成分以及狀態遷移時的告警和操作。Kripke結構中的每個狀態實際上都可用每個狀態均賦值的元組（tuple）來表示。Kripke結構中的狀態遷移表征了一個或多個狀態變量取值的變化；而且還可以比較通過擴展給定模型而得到的Kripke結構，對指定的系統屬性進行校驗。然而，為了更好地理解每條屬性語句的含義，Kripke結構還必須進一步擴展為無限樹形結構，其中樹形結構的每個分支都表征了系統可能的執行操作或行為。 路徑和屬性規范 最開始，系統可以處于9個狀態中的任意一個，其中對于A和B的水位沒有任何限制，而pump的初始狀態假定為off。這樣，我們就可以利用有序元組表征狀態，其中A和B分別表示水槽A和B的當前水位，而P則表示pump的當前狀態。例如，可以假定系統的初始狀態為。對于系統模型，初始狀態之后的下一個狀態可以為和中的任意一個。從狀態開始，下一個狀態可以為、、、、或中的任意一個。根據每個狀態，可以計算出下一個可能的狀態。 這些狀態可以無限執行（或運算）樹狀結構的形式進行排列。如圖3所示，樹根為我們所選的初始狀態，任意狀態的分支均表示下一個可能的狀態，而每個系統執行都是執行樹狀結構的一條路徑。總體上，系統可以具有無限多個這樣的執行路徑。模型校驗的目標就是檢驗執行樹狀結構是否滿足用戶指定的屬性要求。 現在的問題在于，我們究竟該如何描述執行樹狀結構路徑（及路徑上的狀態）的屬性。從技術的角度看，運算樹邏輯（Computation tree logic, CTL）是時序邏輯（time temporal logic, TTL）的一個分支，其簡單性和直觀性非常適合于本例。CTL是常用的布爾命題邏輯（Boolean propositional logic, BPL）的擴展，除了支持包括“和（and）”、“或（or）”、“否（not）”、“蘊涵（implies）”在內的BPL邏輯連接操作外，還支持輔助的時序連接操作。表2所示為 CTL 中的某些連接操作。 表1和圖4說明了CTL中一些基本時序連接操作的直觀意義。一般地，E（就某個路徑而言）和A（就所有的路徑而言）表示從某個狀態開始的路徑數目。F（就某個狀態而言）和G（就所有狀態而言）表示某個路徑中的狀態數目。 對于指定的屬性以及對應于系統模型的運算樹T（可以是無限運算樹），模型校驗算法可以通過校驗T判斷T是否滿足該屬性。例如，考慮指定的屬性AF g，其中g表示與任何CTL連接無關的命題公式。圖4b給出了運算樹T的一個示例。如果屬性AF g在根狀態s0的值設定為true（即如果T中的每條路徑中有狀態開始于s0以使公式g為true），那么對于該運算樹TAF g的值為true。如果g在s0為true，那么就實現了預定目標，因為s0將會出現在從s0開始的每條路徑中。但如果g在s0狀態下不為true，由于從s0開始的路徑要么是s0的左分支，要么是s0的右分支，因此如果在運算樹T中s0的兩個分支都為true（通過遞歸校驗），那么該屬性在s0處也為true。 圖4b顯示，g在左分支根部為true（球體填充為黃色）。因此從s0到左分支單元的所有路徑以及整個左分支樹都滿足該屬性。現在假定g在s0的右分支根部不為true；因此對于所有的子單元都將遞歸檢驗該屬性。圖4b顯示，對于s0右分支的所有子單元，g都為true（球體填充為黃色），因此對于s0的右分支樹該屬性為true。這樣，對于s0的所有子分支樹該屬性為true，從而s0也為true。 圖4歸納了類似的其他屬性（例如EG g和AG g）校驗原理。當然，實際應用中的模型校驗算法遠比這復雜；這些算法利用一些巧妙的簡化手段對狀態空間進行精簡，從而避免了對那些確保為true的屬性進行校驗。一些設計良好的模型校驗器可用來校驗狀態數高達1,040個的狀態空間的屬性。在SMV中，待驗證的屬性可由SPEC部分的用戶指定。邏輯連接“否”、“或”、“和”和“if-then”可以分別用!、|、&和 ->表示。CTL時序連接則表示為AF、AG、EF、EG等。屬性AF（pump=on）表示對于每條開始于初始狀態的路徑，路徑中有一個pump=on的狀態。在初始狀態，該屬性顯然為false，因為從初始狀態開始有一條路徑pump的值始終為off（例如，當水槽A永遠保持為空時）。如果希望在SPEC部分中描述該屬性，那么SMV將為該屬性生成如下反例。循環表征了開始于初始狀態的無限狀態序列（換言之，即路徑），這樣水槽B在該路徑下的每個狀態均為Full，因此pump=off。 與嚴格的規范化語言相結合，可以下列執行序列表示： state 1.1: level_a = Full level_b = Full pump = off state 1.2: 屬性AF（pump=off）具有兩重含義，表征的是對于每條開始于初始狀態的路徑，路徑中有一個狀態中pump=off。該屬性當然在初始狀態為true，因為初始狀態本身（所有路徑均包含初始狀態）pump=off就成立。 時序連接和邏輯連接相結合，可以得到一些有趣的復雜屬性。屬性AG（（pump=off） -> AF （pump=on））表示如果pump=off，那么最終pump=on這種情形總會發生。初始狀態，該屬性顯然為false。屬性AG AF （pump=off -> （level_a=Empty | level_b=Full））表示如果底層水槽為Empty或上層水槽為Full，那么pump將總是為off。屬性AG （EF （level_b= ok|level_b=Full））表示總是會出現上層水槽為ok或Full的情形。 實際應用中的模型校驗 模型校驗已被證明是對各類系統（尤其是硬件系統、實時嵌入式系統和安全臨界系統）進行需求和設計驗證的有效工具。例如，SPIN模型校驗器曾用于驗證NASA的深空1發射方案中的多線程規劃執行模型并成功地發現了5個先前未知的并發缺陷。然而，實際使用模型校驗時還需要注意下面一些主要問題： 1. 每種模型校驗工具都采用特有的建模語言，這些建模語言一般都無法將不規范的需求描述自動轉化為規范化語言。這樣的轉化顯然需要手工完成，因此很難檢驗模型是否正確地表示了建模系統。實際上，指定的建模表示法往往很難甚至根本不可能對部分系統需求進行建模。2. 專用工具屬性規范表示法也存在類似的問題，屬性表示法通常可以是CTL、CTL＊或命題線性時序邏輯（PLTL）的變形。某些需要驗證的屬性很難甚至根本不可能用該表示法進行描述。3. 模型系統中的狀態數量也可能極為龐大。盡管模型校驗算法可以利用一些技巧減小狀態空間的復雜度，但模型校驗器仍然需要很長的時間才能驗證一個指定的屬性或者決定“放棄”驗證該屬性。這時，用戶將不得不投入更大的精力，獨立驗證模型的各部分或者通過減小變量的取值范圍以達到簡化狀態空間的目的。 盡管如此，模型校驗仍被證明是無與倫比的系統需求或設計驗證工具。該工具能在需求或設計的早期階段發現瑕疵，因此能極大地節省后續的開發時間。 鳴謝 衷心感謝Tata研發和設計中心（TRDDC）的常務董事Mathai Joseph教授對我的大力支持。我也非常感激Manasee Palshikar博士對我的鼓勵和支持。 參考文獻 1. Clarke, Edmund M., Orna Grumberg, and Doron A. Peled. Model Checking, Cambridge, MA: MIT Press, 1999.2. Berard, Beatrice, Michel Bidoit, Alain Finkel, Francois Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre Mckenzie. Systems and Software Verification: Model-Checking Techniques and Tools, Berlin-Heidelberg: Springer Verlag, 2001. 3. Havelund, Klaus, Mike Lowry, and John Penix. "Formal Analysis of a Space-Craft Controller using SPIN," IEEE Transactions on Software Engineering, vol. 27, no. 8, Aug. 2001, pp. 749-765. 4. Clarke, Edmund M., Orna Grumberg, and Doron A. Peled. Model Checking, Cambridge, MA: MIT Press, 1999. 5. Berard, Beatrice, Michel Bidoit, Alain Finkel, Francois Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre Mckenzie. Systems and Software Verification: Model-Checking Techniques and Tools, Berlin-Heidelberg: Springer Verlag, 2001. 6. Havelund, Klaus, Mike Lowry, and John Penix. "Formal Analysis of a Space-Craft Controller using SPIN," IEEE Transactions on Software Engineering, vol. 27, no. 8, Aug. 2001, pp. 749-765. 7. Harel, David, and Michal Politi. Modeling Reactive Systems with Statecharts—The Statemate Approach. New York, NY: McGraw-Hill, 1998. 作者：Girish Keshav Palshikar，Tata研發和設計中心科學家，Email: girishp@pune.tcs.co.in