最開始，系統(tǒng)可以處于9個(gè)狀態(tài)中的任意一個(gè)，其中對于A和B的水位沒有任何限制，而pump的初始狀態(tài)假定為off。這樣，我們就可以利用有序元組

　　這 些狀態(tài)可以無限執(zhí)行(或運(yùn)算)樹狀結(jié)構(gòu)的形式進(jìn)行排列。如圖3所示，樹根為我們所選的初始狀態(tài)，任意狀態(tài)的分支均表示下一個(gè)可能的狀態(tài)，而每個(gè)系統(tǒng)執(zhí)行都 是執(zhí)行樹狀結(jié)構(gòu)的一條路徑?？傮w上，系統(tǒng)可以具有無限多個(gè)這樣的執(zhí)行路徑。模型校驗(yàn)的目標(biāo)就是檢驗(yàn)執(zhí)行樹狀結(jié)構(gòu)是否滿足用戶指定的屬性要求。

　　現(xiàn) 在的問題在于，我們究竟該如何描述執(zhí)行樹狀結(jié)構(gòu)路徑(及路徑上的狀態(tài))的屬性。從技術(shù)的角度看，運(yùn)算樹邏輯(Computation tree logic, CTL)是時(shí)序邏輯(time temporal logic, TTL)的一個(gè)分支，其簡單性和直觀性非常適合于本例。CTL是常用的布爾命題邏輯(Boolean propositional logic, BPL)的擴(kuò)展，除了支持包括“和(and)”、“或(or)”、“否(not)”、“蘊(yùn)涵(implies)”在內(nèi)的BPL邏輯連接操作外，還支持輔助 的時(shí)序連接操作。表2所示為 CTL 中的某些連接操作。

　　表1和圖4說明了CTL中一些基本時(shí)序連接操作的直觀意義。一般地，E(就某個(gè)路徑而言)和A(就所有的路徑而言)表示從某個(gè)狀態(tài)開始的路徑數(shù)目。F(就某個(gè)狀態(tài)而言)和G(就所有狀態(tài)而言)表示某個(gè)路徑中的狀態(tài)數(shù)目。

　　圖4：狀態(tài)s0處滿足CTL公式的直覺推導(dǎo)。

　　對 于指定的屬性以及對應(yīng)于系統(tǒng)模型的運(yùn)算樹T(可以是無限運(yùn)算樹)，模型校驗(yàn)算法可以通過校驗(yàn)T判斷T是否滿足該屬性。例如，考慮指定的屬性AF g，其中g(shù)表示與任何CTL連接無關(guān)的命題公式。圖4b給出了運(yùn)算樹T的一個(gè)示例。如果屬性AF g在根狀態(tài)s0的值設(shè)定為true(即如果T中的每條路徑中有狀態(tài)開始于s0以使公式g為true)，那么對于該運(yùn)算樹TAF g的值為true。如果g在s0為true，那么就實(shí)現(xiàn)了預(yù)定目標(biāo)，因?yàn)閟0將會出現(xiàn)在從s0開始的每條路徑中。但如果g在s0狀態(tài)下不為true，由于 從s0開始的路徑要么是s0的左分支，要么是s0的右分支，因此如果在運(yùn)算樹T中s0的兩個(gè)分支都為true(通過遞歸校驗(yàn))，那么該屬性在s0處也為 true。

　　圖4b顯示，g在左分支根部為true(球體填充為黃色)。因此從s0到左分支單元的所有路徑以及整個(gè)左分支樹都 滿足該屬性。現(xiàn)在假定g在s0的右分支根部不為true;因此對于所有的子單元都將遞歸檢驗(yàn)該屬性。圖4b顯示，對于s0右分支的所有子單元，g都為 true(球體填充為黃色)，因此對于s0的右分支樹該屬性為true。這樣，對于s0的所有子分支樹該屬性為true，從而s0也為true。

　　圖4 歸納了類似的其他屬性(例如EG g和AG g)校驗(yàn)原理。當(dāng)然，實(shí)際應(yīng)用中的模型校驗(yàn)算法遠(yuǎn)比這復(fù)雜;這些算法利用一些巧妙的簡化手段對狀態(tài)空間進(jìn)行精簡，從而避免了對那些確保為true的屬性進(jìn) 行校驗(yàn)。一些設(shè)計(jì)良好的模型校驗(yàn)器可用來校驗(yàn)狀態(tài)數(shù)高達(dá)1,040個(gè)的狀態(tài)空間的屬性。在SMV中，待驗(yàn)證的屬性可由SPEC部分的用戶指定。邏輯連接 “否”、“或”、“和”和“if-then”可以分別用!、|、和 ->表示。CTL時(shí)序連接則表示為AF、AG、EF、EG等。屬性AF(pump=on)表示對于每條開始于初始狀態(tài)的路徑，路徑中有一個(gè)pump =on的狀態(tài)。在初始狀態(tài)，該屬性顯然為false，因?yàn)閺某跏紶顟B(tài)開始有一條路徑pump的值始終為off(例如，當(dāng)水槽A永遠(yuǎn)保持為空時(shí))。如果希望 在SPEC部分中描述該屬性，那么SMV將為該屬性生成如下反例。循環(huán)表征了開始于初始狀態(tài)的無限狀態(tài)序列(換言之，即路徑)，這樣水槽B在該路徑下的每 個(gè)狀態(tài)均為Full，因此pump=off。

　　與嚴(yán)格的規(guī)范化語言相結(jié)合，可以下列執(zhí)行序列表示：

　　state 1.1:

　　level_a = Full

　　level_b = Full

　　pump = off

　　state 1.2:

　　屬性AF(pump=off)具有兩重含義，表征的是對于每條開始于初始狀態(tài)的路徑，路徑中有一個(gè)狀態(tài)中pump=off。該屬性當(dāng)然在初始狀態(tài)為true，因?yàn)槌跏紶顟B(tài)本身(所有路徑均包含初始狀態(tài))pump=off就成立。

　　表2：CTL中的一些時(shí)序連接。

　　時(shí) 序連接和邏輯連接相結(jié)合，可以得到一些有趣的復(fù)雜屬性。屬性AG((pump=off) -> AF (pump=on))表示如果pump=off，那么最終pump=on這種情形總會發(fā)生。初始狀態(tài)，該屬性顯然為false。屬性AG AF (pump=off -> (level_a=Empty | level_b=Full))表示如果底層水槽為Empty或上層水槽為Full，那么pump將總是為off。屬性AG (EF (level_b= ok|level_b=Full))表示總是會出現(xiàn)上層水槽為ok或Full的情形。

　　實(shí)際應(yīng)用中的模型校驗(yàn)

　　模型校驗(yàn)已被證明是對各類系統(tǒng)(尤其是硬件系統(tǒng)、實(shí)時(shí)嵌入式系統(tǒng)和安全臨界系統(tǒng))進(jìn)行需求和設(shè)計(jì)驗(yàn)證的有效工具。例如，SPIN模型校驗(yàn)器曾用于驗(yàn)證NASA的深空1發(fā)射方案中的多線程規(guī)劃執(zhí)行模型并成功地發(fā)現(xiàn)了5個(gè)先前未知的并發(fā)缺陷。然而，實(shí)際使用模型校驗(yàn)時(shí)還需要注意下面一些主要問題：

　　1. 每種模型校驗(yàn)工具都采用特有的建模語言，這些建模語言一般都無法將不規(guī)范的需求描述自動轉(zhuǎn)化為規(guī)范化語言。這樣的轉(zhuǎn)化顯然需要手工完成，因此很難檢驗(yàn)?zāi)Ｐ?是否正確地表示了建模系統(tǒng)。實(shí)際上，指定的建模表示法往往很難甚至根本不可能對部分系統(tǒng)需求進(jìn)行建模。2. 專用工具屬性規(guī)范表示法也存在類似的問題，屬性表示法通?？梢允荂TL、CTL*或命題線性時(shí)序邏輯(PLTL)的變形。某些需要驗(yàn)證的屬性很難甚至根本 不可能用該表示法進(jìn)行描述。3. 模型系統(tǒng)中的狀態(tài)數(shù)量也可能極為龐大。盡管模型校驗(yàn)算法可以利用一些技巧減小狀態(tài)空間的復(fù)雜度，但模型校驗(yàn)器仍然需要很長的時(shí)間才能驗(yàn)證一個(gè)指定的屬性或 者決定“放棄”驗(yàn)證該屬性。這時(shí)，用戶將不得不投入更大的精力，獨(dú)立驗(yàn)證模型的各部分或者通過減小變量的取值范圍以達(dá)到簡化狀態(tài)空間的目的。

　　盡管如此，模型校驗(yàn)仍被證明是無與倫比的系統(tǒng)需求或設(shè)計(jì)驗(yàn)證工具。該工具能在需求或設(shè)計(jì)的早期階段發(fā)現(xiàn)瑕疵，因此能極大地節(jié)省后續(xù)的開發(fā)時(shí)間。