SMV系統
SMV 2.5.4版
作者：K.L. 麥克米蘭
電子郵箱:mcmillan@cs.cmu.edu
初稿完成日：1992年2月2日
最後修訂日：2000年11月6日
SMV系統是在時序邏輯CTL中檢驗有窮狀態系統是否超標的工具。其輸入語言允許從完全同步到完全異步，以及從具體到抽象地描述有窮狀態系統。它易於指定壹個系統為米利機，或為壹個抽象、非定常過程的異步網絡。該語言提供模塊化分層描述和可重用機構定義。由於它被設計成描述有限狀態機，該語言數據內型只能使用有限數據，如布爾值、標量型變量，固定數組，靜態的、結構化數據內型也能夠被構造。邏輯CTL能把壹大批時序屬性,如安全性、活躍性、清晰性、去死鎖指定成簡單的語法結構。SMV使用基於有序二元決策圖的字符模型核算法來有效測定CTL表達的規格是否令人滿意。
SMV語言的首要目的是描述有限克裏普克結構的轉移關系。所有命題演算語法都可以用來描述這種關系。這顯示了它的靈活性，但同時也帶來了前後可能不壹致的風險。例如：邏輯矛盾的存在會導致系統停頓——壹種或多種不能繼續的狀態。這會導致規格失真和描述不可執行。盡管模式檢核過程能查出系統停頓，最好還是在可能的時候用受限制的描述形式來避免這種問題的出現。為此，SMV提供了壹種並行任務語法。SMV中的任務語符近似於單任務數據流語言。通過檢核多重並行任務同壹變量、循環任務和型誤差，翻譯器能確保只使用該任務的機構系統。因此，這種語言片段可以被看作是壹種硬件描述語言，或者壹種程序設計語言。SMV系統絕不是字符模型檢驗技術的最新成就，也不完全是計算機硬件描述語言，簡單說來它只是壹種探尋以字符模型檢驗方法進行硬件驗證的應用可能性的實驗工具。
本文將介紹SMV系統輸入語言的語法和字符，和SMV模型檢驗器的功能。同時還將介紹該模型檢驗器的壹些能調整性能的可選備用件,並將給出壹些應用實例。所有這些實例都可以用本系統軟件實現。若需知該模型檢驗器的所有功能，請參閱軟件內附帶的《ULIX程序員操作指南》。
壹、輸入語言
在深入研究該語法和字符之前，讓我們來看壹些能闡明其基本原理的簡單例子。先看看下面這個使用該語言的壹段程序：
MODULE main
VAR
request :Boolean
state:{ready,busy};
ASSIGN
init(state):=ready;
next(state:=case
state=ready&request :busy;
1:{ready,busy};
esac;
SPEC
AG(request ?AF state= busy)
輸入文件介紹了模式和規範，其模式是壹個由狀態變量集定義的布爾類型或標量類型的克裏普克結構。上例中，變量“request”被定義為壹個布爾值，變量狀態是個能表征字符值“ready”或“busy”的標量，標量變量值由翻譯器用壹串布爾變量值進行編碼，這樣壹來轉移關系就可用有序二元決策圖表達出來。但是，編碼過程是對用戶不可見的。
克裏普克結構和其初始狀態的轉移關系，由被關鍵字“ASSIGN”引入的並行任務集決定，在上程序中，變量“state”的初始值被設置成了“ready”，通過指定表達值，變量“state”接下來的值由系統當前狀態決定。
case
state=ready&request:busy;
1:{ready,busy};
esac;
如左側的條件成立，格表達值則由右側第壹個表達式決定。因而，如果
state=ready&request
成立，則該表達式的結果是“busy”，否則，將會是設置{ready,busy}。如果壹個設置被指定成變量，結果將是不確定性選項。因而，如果“status”的值不是“ready”,或者“resquest”是個虛值(在當前狀態下),下壹個狀態的“status”值將會是“ready”或者“busy”。不確定選項有助於描述未完全執行的系統(即：設計選項偏離實作項)或狀態變量值不能被完全確定的復合協議的抽象模型。
請註意變量“request”在程序中沒被指定，這讓它可以選擇任何值，賦予其系統輸入自由的特征。
系統規格作為在CTL中的壹個在關鍵字“SPEC”下面的公式而出現。SMV模型檢驗器將核實所有可能的初始狀態均符合規格要求。在這個例子中，系統規格為：如果“request”成立，則系統以不變量運行，然後斷定“state”的值是“busy”。
接下來的例子闡明了可重復使用的模塊和表達式。它是壹個三位二進制計數電路模型。需要註意模塊名“main”在SMV中有特別的意思，就和它在C語言中壹樣。在輸入文件中，模塊定義命令是無關緊要的。
MODULE main
VAR
bit0:counter_cell(1);
bit1: counter_cell(bit0.carry-out);
bit2: counter_cell(bit1.carry-out);
SPEC
AG AF bit2.carry_out
MODULE counter_cell(carry in)
VAR
value:boolean;
ASSIGN
init(value):=0;
next(value):=value+carry_in mod 2;
DEFINE
carry_out :=value & carry_in;
在這例子中，我們可以看到壹個變量也可以為引用的用戶自定義模塊。本例中,模塊“counter_cell”被引用三次，分別命名為“bit0”、“bit1”、“bit2”。它有壹個正式參數“carry in”。在“bit0”中,這個參數被賦值“1”。在“bit1”中, 這個參數被賦值表達式“bit0.carry-out”。這個表達式在“ main”模塊中被求值。但是，“a.b”這種形式的表達式表示“b”屬於模塊“a”，就象a是標準編程語言中的壹個數據結構。因此，“bit1” 模塊中的“carry_in”就是“bit0” 模塊中的“carry_out”,關鍵字DEFINE用來給字符“carry_out”指定表達式“value & carry_in”。