一種基于模型檢查的嵌入式軟件驗證方法
發布時間：2010-2-26 17:17
發布者：李寬
|
對嵌入式軟件的驗證一般依賴于形式化的方法。 形式化的方法可以對嵌入式軟件系統進行嚴格的規約，并可以對系統進行不同視角的驗證。驗證主要是分析系統是否具有期望的性質。常見的驗證技術主要有模型檢查和定理證明。模型檢查自動化程度高，并且當系統不具有期望性質時能給出反例，但它存在狀態爆炸問題。定理證明能基于無窮狀態空間分析，但是自動化程度不高，需要人工干預，并且在證明失敗后不能給出易于理解的反例。本文使用符號模型檢查技術來驗證嵌入式軟件系統，并通過觸摸屏檢測算法來說明該方法的應用。 1 模型檢查 模型檢查是一種驗證有限狀態系統的自動化技術，使用時序邏輯來描述系統性質。本文使用時序邏輯CTL來描述嵌入式系統滿足的性質。CTL有分支時間和線性時間2種算子，其中分支時間算子是指路徑量詞A(“對所有計算路徑”)和E(“對某些計算路徑”)，線性時間算子包括G(“always”，總是)、F(“somet：imes”，有時)、X(“next-time”，下一時刻)和U(“until”，直到)。其中線性時間算子G、F、X和U之前必須有1個路徑量詞。如圖1所示，CTL公式用于描述有限狀態系統上計算路徑的相關性質。圖1(a)表示EFg，即“存在一條計算路徑，在某個狀態，布爾量公式g為真”；圖1(b)表示AFg，即“對所有計算路徑，在每個計算路徑的某個狀態，布爾量公式g為真”；圖1(c)表示EG，即“存在一條計算路徑，在此路徑的所有狀態，布爾量公式g為真”；圖1(d)表示AG，即“在所有計算路徑的所有狀態，布爾量公式g都為真”。 
2 模型檢查工具SMV 常見的模型檢查工具有貝爾實驗室開發的SPIN、赫爾辛基工業大學計算機理論實驗室開發的PR()D和MA—RIA、美國CMU計算機學院開發的SMV等。本文使用SMV作為對嵌入式軟件驗證的模型檢查工具。 SMV基于“符號模型檢查”(Symbolic Model Claec-king)技術，開始是為了研究符號模型檢查應用的可能性而開發的一種對硬件進行檢查的實驗工具，現在已經發展成為廣為流行的分析有限狀態系統的常用工具。 本文中，軟件系統模型用SMV語言描述。1個SMV程序由2部分組成：1個有限狀態轉換系統和1組CTL公式。SMV把初始狀態和轉換關系表示成二叉樹圖BDD(Binary Deciding Diagram)，CTL公式表示系統模型的屬性，也表示成BDD。通過模型檢查算法遍歷系統狀態空間，給出1個聲明的屬性是正確或者不正確的驗證結果，并給出1個不滿足該屬性的反例。1個CTL公式真正的值通過遍歷狀態圖的方式確定，這種遍歷的時間復雜性和狀態空間大小、公式的長度成線性關系。 3 觸摸屏檢測軟件代碼的驗證 觸摸屏作為人機界面的輸入設備已經廣泛應用于各種嵌入式系統中，如手持設備、工業控制、車載設備等。對于有些應用，觸摸屏是關鍵的輸入設備，觸摸屏失效會導致整個系統不可用。因此設計高效、清晰、可靠的觸摸屏驅動程序非常重要。本文使用有限狀態機來描述觸摸屏檢測算法，然后使用SMV語言來描述此有限狀態系統模型，最后使用SMV工具對此模型進行驗證。 3．1 觸摸屏檢測的有限狀態機 本文為了描述的簡單，簡化了觸摸屏檢測的過程。如圖2所示，將觸摸屏檢測分為5個狀態：觸摸屏空閑(Tou-ch-Idle)、觸摸屏抬起狀態 (Touch_Up)、觸摸屏按下檢測狀態(Touch_ChkDown)、觸摸屏按下狀態(Touch_Down)以及觸摸屏抬起檢測狀態 (Touch_ChkUp)。觸摸屏狀態機是由事件觸發來進行狀態變換的，觸發事件有觸筆按下中斷、觸筆按下消抖定時溢出、觸筆抬起中斷、觸筆抬起消抖定時溢出。
3．2 觸摸屏檢測的SMV模型 本節使用SMV語言對3．1節描述的觸摸屏檢測有限狀態機進行建模，具體描述如下：
上述語言描述中，模塊Touch_Detect()是觸摸屏檢測有限狀態機的實現，它有3個布爾量參數：pen_irq、 d_jittery_delay和u_jittery_delay。其中pen_irq表示觸筆中斷，當pen_irq為1時，表示觸筆沒有按下，為0時表示有觸筆按下中斷；d_jittery_delay為1表示觸筆按下消抖時間到；u_jittery_delay表示觸筆抬起消抖時間到。 本文主要驗證了觸摸屏檢測狀態機的可達屬性。屬性用公式(1)和(2)描述。公式(1)的含義是，從檢測狀態為抬起并其觸筆無按下開始的所有計算路徑中，總存在1條計算路徑，能夠到達檢測狀態為按下。公式(2)的含義是，從檢測狀態為按下并其觸筆為按下開始的所有計算路徑中，總存在1條計算路徑，能夠到達檢測狀態為抬起。 3．3 驗證結果
在Intel CPU通過這個驗證結果，可知3．2節中描述的觸摸屏檢測算法模型滿足狀態可達性。 4 總結 本文采用有限狀態機對嵌入式軟件進行建模，使用SMV語言描述狀態機模型，并通過符號模型檢查工具SMV對SMV語言描述的狀態機模型進行驗證。嵌入式軟件系統的正確性、可靠性占據至關重要的地位�；谀Ｐ蜋z查的驗證方法可以在嵌入式軟件開發的早期發現錯誤，從而避免大量重復性的勞動，減少導致嚴重后果的因素。 參考文獻 1. Gannon J D.Purtilo J M.Zelkowitz M V Software Specification:A Comparison of Formal Methods 1994 2. Clarke E M.Emerson E A.Sistla A P Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specification 1986(2) 3. McMillan K L The SMV System 1992 作者：中國電子科技集團公司第三十八研究所 陳波 廖穎 來源：單片機與嵌入式系統應用 2009（5） |
網友評論