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

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

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

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

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

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

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