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