基于有限狀態(tài)機的嵌入式系統模型校驗技術(shù)

模型校驗是最成功的需求驗證工具。模型校驗的基本原理如圖1所示。模型校驗工具的輸入是系統需求或設計(稱(chēng)為模型)以及最終系統期望實(shí)現的特性(稱(chēng)為“規 范”)。如果給定的模型滿(mǎn)足給定的規范，那么工具將輸出yes，否則將生成反例。反例詳細描述了模型無(wú)法滿(mǎn)足規范的原因，通過(guò)研究反例，可以精確地定位模 型的缺陷，如此反復。該方法的原理是通過(guò)確保模型滿(mǎn)足足夠多的系統特性以增強我們對模型正確性的信心。系統需求之所以稱(chēng)為模型，因為這些模型表征的是需求 或設計。

圖1：模型校驗方法。

　　那 么，哪種規范化語(yǔ)言可以用來(lái)定義模型呢?答案當然不是唯一的，因為不同應用領(lǐng)域的需求(或設計)差異很大。例如，銀行系統和空間系統在系統規模、結構、復 雜度、系統數據的屬性及執行操作上的需求差異就很明顯。相反，大多數實(shí)時(shí)嵌入式或安全臨界系統都面向控制，而不是數據，這意味著(zhù)這些系統的動(dòng)態(tài)特性遠比業(yè) 務(wù)邏輯(由系統維護的內部數據的結構及操作)重要。這些基于控制的系統可以應用于諸多領(lǐng)域：航天系統、航空電子、汽車(chē)系統、生物醫學(xué)儀器、工業(yè)自動(dòng)化及過(guò) 程控制、鐵路、核電站等。甚至數字硬件系統的通信和安全協(xié)議均可視為面向控制的系統。

對于面向控制的系統，可以采用有限狀態(tài) 機(FSM)定義需求和設計，這是一種得到廣泛認可的抽象表示方法。當然，光靠FSM并不能對復雜的實(shí)際工業(yè)系統進(jìn)行建模。我們還需要：1. 能將需求模塊化并區分需求等級;2. 能合并各組成部分的需求(或設計);3. 能通過(guò)更新預先規定的變量和設備，防止可能出現的異常。

校驗設計需求時(shí)，通?？梢酝ㄟ^(guò)回答一些問(wèn)題得到結果。下面給出了校驗需求時(shí)最常問(wèn)的一些問(wèn)題：
* 設計需求是否準確地反映了用戶(hù)需求?需求中的每一事項是否與用戶(hù)的期望一致?需求是否包含用戶(hù)所要求的全部?jì)热?
* 設計需求是否表述清晰并無(wú)異義?是否能被用戶(hù)很好地理解?
* 設計需求是否具有靈活性和可實(shí)現性?例如設計需求是否模塊化并具有良好的架構，從而有助于設計和開(kāi)發(fā)?
* 設計需求是否能輕松地定義驗收測試示例以驗證設計實(shí)現與需求的一致性。
* 設計需求是否只是概要地描述而與具體的設計、實(shí)現及技術(shù)平臺等無(wú)關(guān)，從而使得設計人員和開(kāi)發(fā)人員具有充分的自由度實(shí)現這些需求?

回 答這些問(wèn)題當然絕非輕而易舉而且也沒(méi)有任何捷徑可循，但如果需求成功地超越了這些條條框框，那么無(wú)疑為優(yōu)良系統的設計打下了堅實(shí)基礎。盡管可以利用類(lèi)似 UML這樣的建模工具，但仍然需要確保設計需求的質(zhì)量。這個(gè)過(guò)程需要投入大量精力和時(shí)間，包括各種形式的審查，有時(shí)甚至還需要進(jìn)行部分原型設計。此外，需 求設計中采用多種表示方法(如UML中的表示方法)通常又將引發(fā)其他的問(wèn)題,例如:

* 設計需求需要使用哪種表示方法?
* 如何確保不同表示方法的描述的一致性?

圖2：簡(jiǎn)單的雙水槽泵控系統。

設計需求缺陷的成本通常很高，至少需要重設計并進(jìn)行維護。錯誤的需求導致錯誤的系統行為并顯著(zhù)增加成本，如喪失產(chǎn)品的時(shí)效性和本質(zhì)特征，而對于工作在實(shí)時(shí)環(huán)境下的嵌入式安全臨界系統更是如此。為確保系統設計的質(zhì)量，也需要考慮類(lèi)似的問(wèn)題。

改 進(jìn)需求和設計的一條途徑是利用自動(dòng)化工具對需求和設計各環(huán)節的質(zhì)量進(jìn)行校驗。那么，哪種工具最適用呢?一般而言，校驗用英文描述的需求或設計極為困難。因 此，必須采用一種清晰嚴格且無(wú)二義的規范化語(yǔ)言對需求進(jìn)行描述。如果這種描述需求和設計的語(yǔ)言具有明確的語(yǔ)義，那么完全可以開(kāi)發(fā)出自動(dòng)化工具以分析這種語(yǔ) 言描述的設計需求。這種采用嚴格語(yǔ)言描述需求或設計的基本思想已成為系統驗證的基石。

簡(jiǎn)單的系統模型實(shí)例

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

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

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

該系統的模型的SMV建模如表1所示。起始的VAR部分定義了系統的3個(gè)狀態(tài)變量，變量level_a和level_b分別記錄了上層水槽(upper tank)和下層水槽(lowertank)的當前水位;在每個(gè)“時(shí)刻”，這兩個(gè)變量都將分別賦值，取值范圍為Empty、ok或Full。變量pump表征了泵的啟動(dòng)(on)和停止(off)。

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

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

ASSIGN部分定義了系統如何從一個(gè)狀態(tài)遷移到另一個(gè)狀態(tài)。每個(gè)next語(yǔ)句都規定了特定變量的取值變化。所 有這些賦值語(yǔ)句都假定可以并行執行;next語(yǔ)句定義為在該部分執行所有賦值語(yǔ)句后的最終結果。下層水槽的狀態(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)。 上層水槽也可規定類(lèi)似的操作。

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

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

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

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

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

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

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

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

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

state 1.1:
level_a = Full
level_b = Full
pump = off
state 1.2:

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

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

時(shí) 序連接和邏輯連接相結合，可以得到一些有趣的復雜屬性。屬性AG((pump=off) -> AF (pump=on))表示如果pump=off，那么最終pump=on這種情形總會(huì )發(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))表示總是會(huì )出現上層水槽為ok或Full的情形。

　　實(shí)際應用中的模型校驗

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

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

盡管如此，模型校驗仍被證明是無(wú)與倫比的系統需求或設計驗證工具。該工具能在需求或設計的早期階段發(fā)現瑕疵，因此能極大地節省后續的開(kāi)發(fā)時(shí)間。