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

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

　　最 初，兩個水槽均為空。一旦水槽A的水位值為ok(從空開始)，啟動泵并假定水槽B尚未為滿。只要水槽A不為空且水槽B不為滿，泵將持續(xù)工作。一旦水槽A為 空或水槽B為滿，泵將停止工作。一旦泵啟動(或停止)，系統(tǒng)將不會嘗試停止(或啟動)泵。雖然這個示例非常簡單，但可以很容易地擴展為控制多個源水槽和接 收水槽的復(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個狀態(tài)變量，變量level_a和level_b分別記錄了上層水槽(upper tank)和下層水槽(lower

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

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

　　系 統(tǒng)狀態(tài)就可用上述3個變量的不同取值來表示。例如(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，而其他兩個變量則可 取任意值)。

　　ASSIGN部分定義了系統(tǒng)如何從一個狀態(tài)遷移到另一個狀態(tài)。每個next語句都規(guī)定了特定變量的取值變化。所 有這些賦值語句都假定可以并行執(zhí)行;next語句定義為在該部分執(zhí)行所有賦值語句后的最終結(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)無法發(fā)生狀態(tài)遷移;如果泵狀態(tài)為on，則可遷移到ok或Full狀態(tài)。 上層水槽也可規(guī)定類似的操作。

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