模型校驗(yàn)是最成功的需求驗(yàn)證工具。模型校驗(yàn)的基本原理如圖1所示。模型校驗(yàn)工具的輸入是系統(tǒng)需求或設(shè)計(jì)（稱為模型）以及最終系統(tǒng)期望實(shí)現(xiàn)的特性（稱為“規(guī) 范”）。如果給定的模型滿足給定的規(guī)范，那么工具將輸出yes，否則將生成反例。反例詳細(xì)描述了模型無法滿足規(guī)范的原因，通過研究反例，可以精確地定位模 型的缺陷，如此反復(fù)。該方法的原理是通過確保模型滿足足夠多的系統(tǒng)特性以增強(qiáng)我們對模型正確性的信心。系統(tǒng)需求之所以稱為模型，因?yàn)檫@些模型表征的是需求 或設(shè)計(jì)。
　　
　　圖1：模型校驗(yàn)方法。
　　那 么，哪種規(guī)范化語言可以用來定義模型呢？答案當(dāng)然不是唯一的，因?yàn)椴煌瑧?yīng)用領(lǐng)域的需求（或設(shè)計(jì)）差異很大。例如，銀行系統(tǒng)和空間系統(tǒng)在系統(tǒng)規(guī)模、結(jié)構(gòu)、復(fù) 雜度、系統(tǒng)數(shù)據(jù)的屬性及執(zhí)行操作上的需求差異就很明顯。相反，大多數(shù)實(shí)時(shí)嵌入式或安全臨界系統(tǒng)都面向控制，而不是數(shù)據(jù)，這意味著這些系統(tǒng)的動態(tài)特性遠(yuǎn)比業(yè) 務(wù)邏輯（由系統(tǒng)維護(hù)的內(nèi)部數(shù)據(jù)的結(jié)構(gòu)及操作）重要。這些基于控制的系統(tǒng)可以應(yīng)用于諸多領(lǐng)域：航天系統(tǒng)、航空電子、汽車系統(tǒng)、生物醫(yī)學(xué)儀器、工業(yè)自動化及過 程控制、鐵路、核電站等。甚至數(shù)字硬件系統(tǒng)的通信和安全協(xié)議均可視為面向控制的系統(tǒng)。
　　對于面向控制的系統(tǒng)，可以采用有限狀態(tài) 機(jī)（FSM）定義需求和設(shè)計(jì)，這是一種得到廣泛認(rèn)可的抽象表示方法。當(dāng)然，光靠FSM并不能對復(fù)雜的實(shí)際工業(yè)系統(tǒng)進(jìn)行建模。我們還需要：1. 能將需求模塊化并區(qū)分需求等級;2. 能合并各組成部分的需求（或設(shè)計(jì)）;3. 能通過更新預(yù)先規(guī)定的變量和設(shè)備，防止可能出現(xiàn)的異常。
　　校驗(yàn)設(shè)計(jì)需求時(shí)，通常可以通過回答一些問題得到結(jié)果。下面給出了校驗(yàn)需求時(shí)最常問的一些問題：
　　* 設(shè)計(jì)需求是否準(zhǔn)確地反映了用戶需求？需求中的每一事項(xiàng)是否與用戶的期望一致？需求是否包含用戶所要求的全部內(nèi)容？
　　* 設(shè)計(jì)需求是否表述清晰并無異義？是否能被用戶很好地理解？
　　* 設(shè)計(jì)需求是否具有靈活性和可實(shí)現(xiàn)性？例如設(shè)計(jì)需求是否模塊化并具有良好的架構(gòu)，從而有助于設(shè)計(jì)和開發(fā)？
　　* 設(shè)計(jì)需求是否能輕松地定義驗(yàn)收測試示例以驗(yàn)證設(shè)計(jì)實(shí)現(xiàn)與需求的一致性。
　　* 設(shè)計(jì)需求是否只是概要地描述而與具體的設(shè)計(jì)、實(shí)現(xiàn)及技術(shù)平臺等無關(guān)，從而使得設(shè)計(jì)人員和開發(fā)人員具有充分的自由度實(shí)現(xiàn)這些需求？
　　回 答這些問題當(dāng)然絕非輕而易舉而且也沒有任何捷徑可循，但如果需求成功地超越了這些條條框框，那么無疑為優(yōu)良系統(tǒng)的設(shè)計(jì)打下了堅(jiān)實(shí)基礎(chǔ)。盡管可以利用類似 UML這樣的建模工具，但仍然需要確保設(shè)計(jì)需求的質(zhì)量。這個(gè)過程需要投入大量精力和時(shí)間，包括各種形式的審查，有時(shí)甚至還需要進(jìn)行部分原型設(shè)計(jì)。此外，需 求設(shè)計(jì)中采用多種表示方法（如UML中的表示方法）通常又將引發(fā)其他的問題，例如：
　　* 設(shè)計(jì)需求需要使用哪種表示方法？
　　* 如何確保不同表示方法的描述的一致性？
　　
　　圖2：簡單的雙水槽泵控系統(tǒng)。
　　設(shè)計(jì)需求缺陷的成本通常很高，至少需要重設(shè)計(jì)并進(jìn)行維護(hù)。錯誤的需求導(dǎo)致錯誤的系統(tǒng)行為并顯著增加成本，如喪失產(chǎn)品的時(shí)效性和本質(zhì)特征，而對于工作在實(shí)時(shí)環(huán)境下的嵌入式安全臨界系統(tǒng)更是如此。為確保系統(tǒng)設(shè)計(jì)的質(zhì)量，也需要考慮類似的問題。
　　改 進(jìn)需求和設(shè)計(jì)的一條途徑是利用自動化工具對需求和設(shè)計(jì)各環(huán)節(jié)的質(zhì)量進(jìn)行校驗(yàn)。那么，哪種工具最適用呢？一般而言，校驗(yàn)用英文描述的需求或設(shè)計(jì)極為困難。因 此，必須采用一種清晰嚴(yán)格且無二義的規(guī)范化語言對需求進(jìn)行描述。如果這種描述需求和設(shè)計(jì)的語言具有明確的語義，那么完全可以開發(fā)出自動化工具以分析這種語 言描述的設(shè)計(jì)需求。這種采用嚴(yán)格語言描述需求或設(shè)計(jì)的基本思想已成為系統(tǒng)驗(yàn)證的基石。