近十年以來，計算機科學研究的進步大大推動了需求和設計驗證工具和技術的發展，其中最成功的技術當屬模型校驗。模型驗證與規范化建模語言的緊密結合，極大地推動了驗證自動化的發展。本文介紹了模型校驗的原理及工作方式。

    模型校驗是最成功的需求驗證工具。模型校驗的基本原理如圖1所示。模型校驗工具的輸入是系統需求或設計(稱為模型)以及最終系統期望實現的特性(稱為“規范”)。如果給定的模型滿足給定的規范，那么工具將輸出yes，否則將生成反例。反例詳細描述了模型無法滿足規范的原因，通過研究反例，可以精確地定位模型的缺陷，如此反復。該方法的原理是通過確保模型滿足足夠多的系統特性以增強我們對模型正確性的信心。系統需求之所以稱為模型，因為這些模型表征的是需求或設計。

圖1：模型校驗方法。

    那么，哪種規范化語言可以用來定義模型呢？答案當然不是唯一的，因為不同應用領域的需求(或設計)差異很大。例如，銀行系統和空間系統在系統規模、結構、復雜度、系統數據的屬性及執行操作上的需求差異就很明顯。相反，大多數實時嵌入式或安全臨界系統都面向控制，而不是數據，這意味著這些系統的動態特性遠比業務邏輯(由系統維護的內部數據的結構及操作)重要。這些基于控制的系統可以應用于諸多領域：航天系統、航空電子、汽車系統、生物醫學儀器、工業自動化及過程控制、鐵路、核電站等。甚至數字硬件系統的通信和安全協議均可視為面向控制的系統。

    對于面向控制的系統，可以采用有限狀態機(FSM)定義需求和設計，這是一種得到廣泛認可的抽象表示方法。當然，光靠FSM并不能對復雜的實際工業系統進行建模。我們還需要：1. 能將需求模塊化并區分需求等級；2. 能合并各組成部分的需求(或設計)；3. 能通過更新預先規定的變量和設備，防止可能出現的異常。

    校驗設計需求時，通常可以通過回答一些問題得到結果。下面給出了校驗需求時最常問的一些問題：

* 設計需求是否準確地反映了用戶需求？需求中的每一事項是否與用戶的期望一致？需求是否包含用戶所要求的全部內容？
* 設計需求是否表述清晰并無異義？是否能被用戶很好地理解？
* 設計需求是否具有靈活性和可實現性？例如設計需求是否模塊化并具有良好的架構，從而有助于設計和開發？
* 設計需求是否能輕松地定義驗收測試示例以驗證設計實現與需求的一致性。
* 設計需求是否只是概要地描述而與具體的設計、實現及技術平臺等無關，從而使得設計人員和開發人員具有充分的自由度實現這些需求？

    回答這些問題當然絕非輕而易舉而且也沒有任何捷徑可循，但如果需求成功地超越了這些條條框框，那么無疑為優良系統的設計打下了堅實基礎。盡管可以利用類似UML這樣的建模工具，但仍然需要確保設計需求的質量。這個過程需要投入大量精力和時間，包括各種形式的審查，有時甚至還需要進行部分原型設計。此外，需求設計中采用多種表示方法(如UML中的表示方法)通常又將引發其他的問題,例如:

* 設計需求需要使用哪種表示方法？
* 如何確保不同表示方法的描述的一致性？

圖2：簡單的雙水槽泵控系統。

    設計需求缺陷的成本通常很高，至少需要重設計并進行維護。錯誤的需求導致錯誤的系統行為并顯著增加成本，如喪失產品的時效性和本質特征，而對于工作在實時環境下的嵌入式安全臨界系統更是如此。為確保系統設計的質量，也需要考慮類似的問題。

    改進需求和設計的一條途徑是利用自動化工具對需求和設計各環節的質量進行校驗。那么，哪種工具最適用呢？一般而言，校驗用英文描述的需求或設計極為困難。因此，必須采用一種清晰嚴格且無二義的規范化語言對需求進行描述。如果這種描述需求和設計的語言具有明確的語義，那么完全可以開發出自動化工具以分析這種語言描述的設計需求。這種采用嚴格語言描述需求或設計的基本思想已成為系統驗證的基石。

簡單的系統模型實例

    首先，讓我們考察一下如何利用模型校驗工具驗證簡單的嵌入式系統特性。為此，我們采用Carnegie-Mellon大學開發的符號模型驗證器(symbolic model verifier,SMV)作為模型校驗工具。當然，我們也可以采用其他的模型校驗工具描述該模型。文章結束部分列出了可選的模型校驗工具及獲取方式。

    如圖2所示，一個簡單的泵控系統通過泵P將源水槽A中的水傳送至接收水槽B。每個水槽都具有兩級刻度線：一個用來檢測水位是否為空(Empty)，而另一個用來檢測水位是否