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

模型校驗是最成功的需求驗證工具。模型校驗的基本原理如圖1所示。模型校驗工具的輸入是系統(tǒng)需求或設計（稱為模型）以及最終系統(tǒng)期望實現(xiàn)的特性（稱為“規(guī) 范”）。如果給定的模型滿足給定的規(guī)范，那么工具將輸出yes，否則將生成反例。反例詳細描述了模型無法滿足規(guī)范的原因，通過研究反例，可以精確地定位模 型的缺陷，如此反復。該方法的原理是通過確保模型滿足足夠多的系統(tǒng)特性以增強我們對模型正確性的信心。系統(tǒng)需求之所以稱為模型，因為這些模型表征的是需求 或設計。
　　
　　圖1：模型校驗方法。
　　那 么，哪種規(guī)范化語言可以用來定義模型呢？答案當然不是唯一的，因為不同應用領域的需求（或設計）差異很大。例如，銀行系統(tǒng)和空間系統(tǒng)在系統(tǒng)規(guī)模、結構、復 雜度、系統(tǒng)數(shù)據(jù)的屬性及執(zhí)行操作上的需求差異就很明顯。相反，大多數(shù)實時嵌入式或安全臨界系統(tǒng)都面向控制，而不是數(shù)據(jù)，這意味著這些系統(tǒng)的動態(tài)特性遠比業(yè) 務邏輯（由系統(tǒng)維護的內部數(shù)據(jù)的結構及操作）重要。這些基于控制的系統(tǒng)可以應用于諸多領域：航天系統(tǒng)、航空電子、汽車系統(tǒng)、生物醫(yī)學儀器、工業(yè)自動化及過 程控制、鐵路、核電站等。甚至數(shù)字硬件系統(tǒng)的通信和安全協(xié)議均可視為面向控制的系統(tǒng)。
　　對于面向控制的系統(tǒng)，可以采用有限狀態(tài) 機（FSM）定義需求和設計，這是一種得到廣泛認可的抽象表示方法。當然，光靠FSM并不能對復雜的實際工業(yè)系統(tǒng)進行建模。我們還需要：1. 能將需求模塊化并區(qū)分需求等級;2. 能合并各組成部分的需求（或設計）;3. 能通過更新預先規(guī)定的變量和設備，防止可能出現(xiàn)的異常。
　　校驗設計需求時，通?？梢酝ㄟ^回答一些問題得到結果。下面給出了校驗需求時最常問的一些問題：
　　* 設計需求是否準確地反映了用戶需求？需求中的每一事項是否與用戶的期望一致？需求是否包含用戶所要求的全部內容？
　　* 設計需求是否表述清晰并無異義？是否能被用戶很好地理解？
　　* 設計需求是否具有靈活性和可實現(xiàn)性？例如設計需求是否模塊化并具有良好的架構，從而有助于設計和開發(fā)？
　　* 設計需求是否能輕松地定義驗收測試示例以驗證設計實現(xiàn)與需求的一致性。
　　* 設計需求是否只是概要地描述而與具體的設計、實現(xiàn)及技術平臺等無關，從而使得設計人員和開發(fā)人員具有充分的自由度實現(xiàn)這些需求？
　　回 答這些問題當然絕非輕而易舉而且也沒有任何捷徑可循，但如果需求成功地超越了這些條條框框，那么無疑為優(yōu)良系統(tǒng)的設計打下了堅實基礎。盡管可以利用類似 UML這樣的建模工具，但仍然需要確保設計需求的質量。這個過程需要投入大量精力和時間，包括各種形式的審查，有時甚至還需要進行部分原型設計。此外，需 求設計中采用多種表示方法（如UML中的表示方法）通常又將引發(fā)其他的問題，例如：
　　* 設計需求需要使用哪種表示方法？
　　* 如何確保不同表示方法的描述的一致性？
　　
　　圖2：簡單的雙水槽泵控系統(tǒng)。
　　設計需求缺陷的成本通常很高，至少需要重設計并進行維護。錯誤的需求導致錯誤的系統(tǒng)行為并顯著增加成本，如喪失產品的時效性和本質特征，而對于工作在實時環(huán)境下的嵌入式安全臨界系統(tǒng)更是如此。為確保系統(tǒng)設計的質量，也需要考慮類似的問題。
　　改 進需求和設計的一條途徑是利用自動化工具對需求和設計各環(huán)節(jié)的質量進行校驗。那么，哪種工具最適用呢？一般而言，校驗用英文描述的需求或設計極為困難。因 此，必須采用一種清晰嚴格且無二義的規(guī)范化語言對需求進行描述。如果這種描述需求和設計的語言具有明確的語義，那么完全可以開發(fā)出自動化工具以分析這種語 言描述的設計需求。這種采用嚴格語言描述需求或設計的基本思想已成為系統(tǒng)驗證的基石。