近十年以來，計算機(jī)科學(xué)研究的進(jìn)步大大推動了需求和設(shè)計驗證工具和技術(shù)的發(fā)展，其中最成功的技術(shù)當(dāng)屬電子、汽車系統(tǒng)、生物醫(yī)學(xué)儀器、工業(yè)自動化及過程控制、鐵路、核電站等。甚至數(shù)字硬件系統(tǒng)的通信和安全協(xié)議均可視為面向控制的系統(tǒng)。

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

校驗設(shè)計需求時，通�？梢酝ㄟ^回答一些問題得到結(jié)果。下面給出了校驗需求時最常問的一些問題：

* 設(shè)計需求是否準(zhǔn)確地反映了用戶需求？需求中的每一事項是否與用戶的期望一致？需求是否包含用戶所要求的全部內(nèi)容？

* 設(shè)計需求是否表述清晰并無異義？是否能被用戶很好地理解？

* 設(shè)計需求是否具有靈活性和可實現(xiàn)性？例如設(shè)計需求是否模塊化并具有良好的架構(gòu)，從而有助于設(shè)計和開發(fā)？

* 設(shè)計需求是否能輕松地定義驗收測試示例以驗證設(shè)計實現(xiàn)與需求的一致性。

* 設(shè)計需求是否只是概要地描述而與具體的設(shè)計、實現(xiàn)及技術(shù)平臺等無關(guān)，從而使得設(shè)計人員和開發(fā)人員具有充分的自由度實現(xiàn)這些需求？

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

* 設(shè)計需求需要使用哪種表示方法？

* 如何確保不同表示方法的描述的一致性？

圖2：簡單的雙水槽泵控系統(tǒng)。

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

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

簡單的系統(tǒng)模型實例

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

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

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