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

　　圖1：模型校驗方法。

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

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

　　校驗設計需求時，通?？梢酝ㄟ^回答一些問題得到結果。下面給出了校驗需求時最常問的一些問題：

　　* 設計需求是否準確地反映了用戶需求?需求中的每一事項是否與用戶的期望一致?需求是否包含用戶所要求的全部內容?

　　* 設計需求是否表述清晰并無異義?是否能被用戶很好地理解?

　　* 設計需求是否具有靈活性和可實現性?例如設計需求是否模塊化并具有良好的架構，從而有助于設計和開發(fā)?

　　* 設計需求是否能輕松地定義驗收測試示例以驗證設計實現與需求的一致性。

　　* 設計需求是否只是概要地描述而與具體的設計、實現及技術平臺等無關，從而使得設計人員和開發(fā)人員具有充分的自由度實現這些需求?

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

　　* 設計需求需要使用哪種表示方法?

　　* 如何確保不同表示方法的描述的一致性?

　　圖2：簡單的雙水槽泵控系統(tǒng)。

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

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