一種基于模型檢查的嵌入式軟件驗(yàn)證方法

    嵌入式軟件廣泛應(yīng)用于不同領(lǐng)域，如消費(fèi)電子、工業(yè)控制、汽車電子、移動(dòng)通信等。嵌入式軟件的可靠性保證十分關(guān)鍵。嵌入式軟件中常見(jiàn)的錯(cuò)誤包括狀態(tài)機(jī)錯(cuò)誤、時(shí)序錯(cuò)誤、棧溢出／存儲(chǔ)溢出等，在開(kāi)發(fā)過(guò)程中對(duì)嵌入式軟件進(jìn)行驗(yàn)證十分重要。
    對(duì)嵌入式軟件的驗(yàn)證一般依賴于形式化的方法。
形式化的方法可以對(duì)嵌入式軟件系統(tǒng)進(jìn)行嚴(yán)格的規(guī)約，并可以對(duì)系統(tǒng)進(jìn)行不同視角的驗(yàn)證。驗(yàn)證主要是分析系統(tǒng)是否具有期望的性質(zhì)。常見(jiàn)的驗(yàn)證技術(shù)主要有模型檢查和定理證明。模型檢查自動(dòng)化程度高，并且當(dāng)系統(tǒng)不具有期望性質(zhì)時(shí)能給出反例，但它存在狀態(tài)爆炸問(wèn)題。定理證明能基于無(wú)窮狀態(tài)空間分析，但是自動(dòng)化程度不高，需要人工干預(yù)，并且在證明失敗后不能給出易于理解的反例。本文使用符號(hào)模型檢查技術(shù)來(lái)驗(yàn)證嵌入式軟件系統(tǒng)，并通過(guò)觸摸屏檢測(cè)算法來(lái)說(shuō)明該方法的應(yīng)用。

1 模型檢查
    模型檢查是一種驗(yàn)證有限狀態(tài)系統(tǒng)的自動(dòng)化技術(shù)，使用時(shí)序邏輯來(lái)描述系統(tǒng)性質(zhì)。本文使用時(shí)序邏輯CTL來(lái)描述嵌入式系統(tǒng)滿足的性質(zhì)。CTL有分支時(shí)間和線性時(shí)間2種算子，其中分支時(shí)間算子是指路徑量詞A(“對(duì)所有計(jì)算路徑”)和E(“對(duì)某些計(jì)算路徑”)，線性時(shí)間算子包括G(“always”，總是)、F(“somet：imes”，有時(shí))、X(“next-time”，下一時(shí)刻)和U(“until”，直到)。其中線性時(shí)間算子G、F、X和U之前必須有1個(gè)路徑量詞。如圖1所示，CTL公式用于描述有限狀態(tài)系統(tǒng)上計(jì)算路徑的相關(guān)性質(zhì)。圖1(a)表示EFg，即“存在一條計(jì)算路徑，在某個(gè)狀態(tài)，布爾量公式g為真”；圖1(b)表示AFg，即“對(duì)所有計(jì)算路徑，在每個(gè)計(jì)算路徑的某個(gè)狀態(tài)，布爾量公式g為真”；圖1(c)表示EG，即“存在一條計(jì)算路徑，在此路徑的所有狀態(tài)，布爾量公式g為真”；圖1(d)表示AG，即“在所有計(jì)算路徑的所有狀態(tài)，布爾量公式g都為真”。

2 模型檢查工具SMV
    常見(jiàn)的模型檢查工具有貝爾實(shí)驗(yàn)室開(kāi)發(fā)的SPIN、赫爾辛基工業(yè)大學(xué)計(jì)算機(jī)理論實(shí)驗(yàn)室開(kāi)發(fā)的PR()D和MA—RIA、美國(guó)CMU計(jì)算機(jī)學(xué)院開(kāi)發(fā)的SMV等。本文使用SMV作為對(duì)嵌入式軟件驗(yàn)證的模型檢查工具。
    SMV基于“符號(hào)模型檢查”(Symbolic Model Claec-king)技術(shù)，開(kāi)始是為了研究符號(hào)模型檢查應(yīng)用的可能性而開(kāi)發(fā)的一種對(duì)硬件進(jìn)行檢查的實(shí)驗(yàn)工具，現(xiàn)在已經(jīng)發(fā)展成為廣為流行的分析有限狀態(tài)系統(tǒng)的常用工具。
    本文中，軟件系統(tǒng)模型用SMV語(yǔ)言描述。1個(gè)SMV程序由2部分組成：1個(gè)有限狀態(tài)轉(zhuǎn)換系統(tǒng)和1組CTL公式。SMV把初始狀態(tài)和轉(zhuǎn)換關(guān)系表示成二叉樹(shù)圖BDD(Binary Deciding Diagram)，CTL公式表示系統(tǒng)模型的屬性，也表示成BDD。通過(guò)模型檢查算法遍歷系統(tǒng)狀態(tài)空間，給出1個(gè)聲明的屬性是正確或者不正確的驗(yàn)證結(jié)果，并給出1個(gè)不滿足該屬性的反例。1個(gè)CTL公式真正的值通過(guò)遍歷狀態(tài)圖的方式確定，這種遍歷的時(shí)間復(fù)雜性和狀態(tài)空間大小、公式的長(zhǎng)度成線性關(guān)系。

3 觸摸屏檢測(cè)軟件代碼的驗(yàn)證
    觸摸屏作為人機(jī)界面的輸入設(shè)備已經(jīng)廣泛應(yīng)用于各種嵌入式系統(tǒng)中，如手持設(shè)備、工業(yè)控制、車載設(shè)備等。對(duì)于有些應(yīng)用，觸摸屏是關(guān)鍵的輸入設(shè)備，觸摸屏失效會(huì)導(dǎo)致整個(gè)系統(tǒng)不可用。因此設(shè)計(jì)高效、清晰、可靠的觸摸屏驅(qū)動(dòng)程序非常重要。本文使用有限狀態(tài)機(jī)來(lái)描述觸摸屏檢測(cè)算法，然后使用SMV語(yǔ)言來(lái)描述此有限狀態(tài)系統(tǒng)模型，最后使用SMV工具對(duì)此模型進(jìn)行驗(yàn)證。
3．1 觸摸屏檢測(cè)的有限狀態(tài)機(jī)
    本文為了描述的簡(jiǎn)單，簡(jiǎn)化了觸摸屏檢測(cè)的過(guò)程。如圖2所示，將觸摸屏檢測(cè)分為5個(gè)狀態(tài)：觸摸屏空閑(Tou-ch-Idle)、觸摸屏抬起狀態(tài)(Touch_Up)、觸摸屏按下檢測(cè)狀態(tài)(Touch_ChkDown)、觸摸屏按下?tīng)顟B(tài)(Touch_Down)以及觸摸屏抬起檢測(cè)狀態(tài)(Touch_ChkUp)。觸摸屏狀態(tài)機(jī)是由事件觸發(fā)來(lái)進(jìn)行狀態(tài)變換的，觸發(fā)事件有觸筆按下中斷、觸筆按下消抖定時(shí)溢出、觸筆抬起中斷、觸筆抬起消抖定時(shí)溢出。

                                [!--empirenews.page--]

3．2 觸摸屏檢測(cè)的SMV模型
    本節(jié)使用SMV語(yǔ)言對(duì)3．1節(jié)描述的觸摸屏檢測(cè)有限狀態(tài)機(jī)進(jìn)行建模，具體描述如下：

    上述語(yǔ)言描述中，模塊Touch_Detect()是觸摸屏檢測(cè)有限狀態(tài)機(jī)的實(shí)現(xiàn)，它有3個(gè)布爾量參數(shù)：pen_irq、d_jittery_delay和u_jittery_delay。其中pen_irq表示觸筆中斷，當(dāng)pen_irq為1時(shí)，表示觸筆沒(méi)有按下，為0時(shí)表示有觸筆按下中斷；d_jittery_delay為1表示觸筆按下消抖時(shí)間到；u_jittery_delay表示觸筆抬起消抖時(shí)間到。
    本文主要驗(yàn)證了觸摸屏檢測(cè)狀態(tài)機(jī)的可達(dá)屬性。屬性用公式(1)和(2)描述。公式(1)的含義是，從檢測(cè)狀態(tài)為抬起并其觸筆無(wú)按下開(kāi)始的所有計(jì)算路徑中，總存在1條計(jì)算路徑，能夠到達(dá)檢測(cè)狀態(tài)為按下。公式(2)的含義是，從檢測(cè)狀態(tài)為按下并其觸筆為按下開(kāi)始的所有計(jì)算路徑中，總存在1條計(jì)算路徑，能夠到達(dá)檢測(cè)狀態(tài)為抬起。
3．3 驗(yàn)證結(jié)果
    在Intel CPU
    通過(guò)這個(gè)驗(yàn)證結(jié)果，可知3．2節(jié)中描述的觸摸屏檢測(cè)算法模型滿足狀態(tài)可達(dá)性。

4 總 結(jié)
    本文采用有限狀態(tài)機(jī)對(duì)嵌入式軟件進(jìn)行建模，使用SMV語(yǔ)言描述狀態(tài)機(jī)模型，并通過(guò)符號(hào)模型檢查工具SMV對(duì)SMV語(yǔ)言描述的狀態(tài)機(jī)模型進(jìn)行驗(yàn)證。嵌入式軟件系統(tǒng)的正確性、可靠性占據(jù)至關(guān)重要的地位。基于模型檢查的驗(yàn)證方法可以在嵌入式軟件開(kāi)發(fā)的早期發(fā)現(xiàn)錯(cuò)誤，從而避免大量重復(fù)性的勞動(dòng)，減少導(dǎo)致嚴(yán)重后果的因素。