實時嵌入式系統模型校驗技術

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

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

　　最 初，兩個水槽均為空。一旦水槽A的水位值為ok(從空開始)，啟動泵并假定水槽B尚未為滿。只要水槽A不為空且水槽B不為滿，泵將持續工作。一旦水槽A為 空或水槽B為滿，泵將停止工作。一旦泵啟動(或停止)，系統將不會嘗試停止(或啟動)泵。雖然這個示例非常簡單，但可以很容易地擴展為控制多個源水槽和接 收水槽的復雜泵管線網絡控制器，如應用在水處理系統或化工廠中的控制器。

　　表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))

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

　　圖3：泵控系統執行樹的初始部分。

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

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

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

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