首 先，讓我們考察一下如何利用模型校驗(yàn)工具驗(yàn)證簡(jiǎn)單的嵌入式系統(tǒng)特性。為此，我們采用Carnegie-Mellon大學(xué)開(kāi)發(fā)的符號(hào)模型驗(yàn)證器 (symbolic model verifier,SMV)作為模型校驗(yàn)工具。當(dāng)然，我們也可以采用其他的模型校驗(yàn)工具描述該模型。文章結(jié)束部分列出了可選的模型校驗(yàn)工具及獲取方式。

　　如 圖2所示，一個(gè)簡(jiǎn)單的泵控系統(tǒng)通過(guò)泵P將源水槽A中的水傳送至接收水槽B。每個(gè)水槽都具有兩級(jí)刻度線：一個(gè)用來(lái)檢測(cè)水位是否為空(Empty)，而另一個(gè) 用來(lái)檢測(cè)水位是否已滿(Full)。如果水槽的水位既不為空也不為滿，那么水槽刻度線設(shè)定為ok;換言之，即水位高于空刻度線但低于滿刻度線。

　　最 初，兩個(gè)水槽均為空。一旦水槽A的水位值為ok(從空開(kāi)始)，啟動(dòng)泵并假定水槽B尚未為滿。只要水槽A不為空且水槽B不為滿，泵將持續(xù)工作。一旦水槽A為 空或水槽B為滿，泵將停止工作。一旦泵啟動(dòng)(或停止)，系統(tǒng)將不會(huì)嘗試停止(或啟動(dòng))泵。雖然這個(gè)示例非常簡(jiǎn)單，但可以很容易地?cái)U(kuò)展為控制多個(gè)源水槽和接 收水槽的復(fù)雜泵管線網(wǎng)絡(luò)控制器，如應(yīng)用在水處理系統(tǒng)或化工廠中的控制器。

　　表1：SMV模型描述和需求清單。

　　MODULE main

　　VAR

　　level_a : {Empty, ok, Full}; -- lower tank

　　level_b : {Empty, ok, Full}; -- upper tank

　　pump : {on, off};

　　ASSIGN

　　next(level_a) := case

　　level_a = Empty : {Empty, ok};

　　level_a = ok pump = off : {ok, Full};

　　level_a = ok pump = on : {ok, Empty, Full};

　　level_a = Full pump = off : Full;

　　level_a = Full pump = on : {ok, Full};

　　1 : {ok, Empty, Full};

　　esac;

　　next(level_b) := case

　　level_b = Empty pump = off : Empty;

　　level_b = Empty pump = on : {Empty, ok};

　　level_b = ok pump = off : {ok, Empty};

　　level_b = ok pump = on : {ok, Empty, Full};

　　level_b = Full pump = off : {ok, Full};

　　level_b = Full pump = on : {ok, Full};

　　1 : {ok, Empty, Full};

　　esac;

　　next(pump) := case

　　pump = off (level_a = ok | level_a = Full)

　　(level_b = Empty | level_b = ok) : on;

　　pump = on (level_a = Empty | level_b = Full) : off;

　　1 : pump; -- keep pump status as it is

　　esac;

　　INIT

　　(pump = off)

　　SPEC

　　-- pump if always off if ground tank is Empty or up tank is Full

　　-- AG AF (pump = off -> (level_a = Empty | level_b = Full))

　　-- it is always possible to reach a state when the up tank is ok or Full

　　AG (EF (level_b = ok | level_b = Full))

　　該系統(tǒng)的模型的SMV建模如表1所示。起始的VAR部分定義了系統(tǒng)的3個(gè)狀態(tài)變量，變量level_a和level_b分別記錄了上層水槽(upper tank)和下層水槽(lower

　　圖3：泵控系統(tǒng)執(zhí)行樹(shù)的初始部分。

　　tank)的當(dāng)前水位;在每個(gè)“時(shí)刻”，這兩個(gè)變量都將分別賦值，取值范圍為Empty、ok或Full。變量pump表征了泵的啟動(dòng)(on)和停止(off)。

　　系 統(tǒng)狀態(tài)就可用上述3個(gè)變量的不同取值來(lái)表示。例如(level_a=Empty, level_b=ok, pump=off)和l (level_a=Empty, level_b=Full, pump=on)就可以表示系統(tǒng)狀態(tài)。在靠近結(jié)尾的INIT部分，定義了這些變量的初始值(這里，最初假定pump的初始值為off，而其他兩個(gè)變量則可 取任意值)。

　　ASSIGN部分定義了系統(tǒng)如何從一個(gè)狀態(tài)遷移到另一個(gè)狀態(tài)。每個(gè)next語(yǔ)句都規(guī)定了特定變量的取值變化。所 有這些賦值語(yǔ)句都假定可以并行執(zhí)行;next語(yǔ)句定義為在該部分執(zhí)行所有賦值語(yǔ)句后的最終結(jié)果。下層水槽的狀態(tài)可以從Empty狀態(tài)遷移到Empty或 ok狀態(tài);從ok狀態(tài)遷移到Empty或Full狀態(tài)，或保持為ok狀態(tài)(如果pump的狀態(tài)為on);從ok狀態(tài)遷移到ok或Full狀態(tài)(如果 pump的狀態(tài)為off);如果pump狀態(tài)為off，那么下層水槽在Full狀態(tài)無(wú)法發(fā)生狀態(tài)遷移;如果泵狀態(tài)為on，則可遷移到ok或Full狀態(tài)。 上層水槽也可規(guī)定類似的操作。

　　在系統(tǒng)內(nèi)部，大多數(shù)模型校驗(yàn)工具通常會(huì)將輸入模型擴(kuò)展為具有Kripke結(jié)構(gòu)的動(dòng)態(tài)系統(tǒng)。擴(kuò)展 過(guò)程包括在EFSM中除去分層結(jié)構(gòu)、并行成分以及狀態(tài)遷移時(shí)的告警和操作。Kripke結(jié)構(gòu)中的每個(gè)狀態(tài)實(shí)際上都可用每個(gè)狀態(tài)均賦值的元組(tuple) 來(lái)表示。Kripke結(jié)構(gòu)中的狀態(tài)遷移表征了一個(gè)或多個(gè)狀態(tài)變量取值的變化;而且還可以比較通過(guò)擴(kuò)展給定模型而得到的Kripke結(jié)構(gòu)，對(duì)指定的系統(tǒng)屬性 進(jìn)行校驗(yàn)。然而，為了更好地理解每條屬性語(yǔ)句的含義，Kripke結(jié)構(gòu)還必須進(jìn)一步擴(kuò)展為無(wú)限樹(shù)形結(jié)構(gòu)，其中樹(shù)形結(jié)構(gòu)的每個(gè)分支都表征了系統(tǒng)可能的執(zhí)行操 作或行為。