NUSMV是一個符號模型檢查器，源于CMU-SMV的重新設(shè)計、實現(xiàn)和擴展，CMU-SMV是CMU［McM93］開發(fā)的基于BDD的原始模型檢查器。NUSMV項目旨在開發(fā)一個最先進的符號模型檢查器，設(shè)計用于技術(shù)轉(zhuǎn)讓項目：它是一個很好的結(jié)構(gòu)化的、開放的、靈活的和有文件化的模型檢查平臺，并且是魯棒的并且接近工業(yè)系統(tǒng)標準CGR00。

　　NUSMV的版本1基本上實現(xiàn)了基于BDD的符號模型檢查。NUSMV的版本2（以下簡稱NUSMV2）繼承了前一版本的所有功能，并在多個方向上進行了擴展〔CCG+02〕。NUSMV2的主要創(chuàng)新之處在于集成了基于命題可滿足性（SAT）的模型檢測技術(shù)〔BCCZ99〕。目前基于SAT的模型檢測正受到人們的青睞在多個工業(yè)領(lǐng)域取得重大成功，開辟了新的研究方向。基于BDD和基于SAT的模型檢查通常能夠解決不同類別的問題，因此可以看作是互補技術(shù)。

　　從NUSMV2開始，我們也采用了一種新的開發(fā)和許可模式。NUSMV2是與一個開源許可證1一起發(fā)布的，它允許任何感興趣的人自由使用該工具并參與其開發(fā)。NUSMV開源項目的目的是為模型檢查社區(qū)提供一個研究、實現(xiàn)和比較新的符號模型檢查技術(shù)的通用平臺。自NUSMV2發(fā)布以來，NUSMV團隊已經(jīng)收到了系統(tǒng)不同部分的代碼貢獻。一些研究機構(gòu)和商業(yè)公司表示有興趣合作開發(fā)NUSMV。NUSMV的主要特點如下：

　　?功能。NUSMV允許同步和異步有限狀態(tài)系統(tǒng)2的表示，并允許使用基于BDD和基于SAT的模型檢查技術(shù)分析以計算樹邏輯（CTL）和線性時序邏輯（LTL）表示的規(guī)范。啟發(fā)式方法可用于實現(xiàn)效率和部分控制狀態(tài)爆炸。與用戶的交互可以通過文本界面進行，也可以在批處理模式下進行。

　　建筑。定義了一個軟件體系結(jié)構(gòu)。NUSMV的不同組成部分和功能在模塊中被隔離和分離。提供了模塊之間的接口。這減少了修改和擴展NUSMV所需的工作量。

　　執(zhí)行質(zhì)量。NUSMV是用ANSI C編寫的，符合POSIX，并且已經(jīng)用Purify進行了調(diào)試，以便檢測內(nèi)存泄漏。此外，對系統(tǒng)代碼進行了徹底的注釋。NUSMV使用了科羅拉多大學(xué)開發(fā)的最新BDD包，并提供了一個通用接口，用于連接最新的SAT解算器。這使得NUSMV非常健壯、可移植、高效，并且容易被開發(fā)人員以外的人理解。

　　在本章中，我們將介紹NUSMV輸入語言的語法和語義。在討論語言的細節(jié)之前，讓我們先給出一些關(guān)于語法的一般注釋。在下面使用的語法符號中，語法類別（非終端）用單空格字體表示，標記和字符集成員（終端）用粗體字體表示。方括號（“［”）中包含的語法結(jié)果是可選的，而豎線（“|”）用于分隔語法規(guī)則中的替代項。有時，在規(guī)則的開頭使用一個of作為在多個備選方案中進行選擇的速記。如果字符|、〔和〕是粗體，它們就失去了特殊的意義，成為常規(guī)的標記。在下面的代碼中，標識符可以是任何字符序列，以集合{a-Za-z}中的一個字符開始，然后是屬于集合{a-Za-z0-9$#-}的一個可能為空的字符序列。標識符中的所有字符和大小寫都是有意義的。空白字符是空格（）、制表符（）和換行符（）。任何以兩個破折號（‘--’）開頭、以換行符結(jié)尾的字符串都是注釋，解析器將忽略這些字符串。多行注釋以“-/--”開頭，以“--/”結(jié)尾。標識符的語法規(guī)則為：