嵌入式軟件廣泛應(yīng)用于不同領(lǐng)域，如消費電子、工業(yè)控制、汽車電子、移動通信等。嵌入式軟件的可靠性保證十分關(guān)鍵。嵌入式軟件中常見的錯誤包括狀態(tài)機(jī)錯誤、時序錯誤、棧溢出／存儲溢出等，在開發(fā)過程中對嵌入式軟件進(jìn)行驗證十分重要。
　　對嵌入式軟件的驗證一般依賴于形式化的方法。
　　形式化的方法可以對嵌入式軟件系統(tǒng)進(jìn)行嚴(yán)格的規(guī)約，并可以對系統(tǒng)進(jìn)行不同視角的驗證。驗證主要是分析系統(tǒng)是否具有期望的性質(zhì)。常見的驗證技術(shù)主要有模型檢查和定理證明。模型檢查自動化程度高，并且當(dāng)系統(tǒng)不具有期望性質(zhì)時能給出反例，但它存在狀態(tài)爆炸問題。定理證明能基于無窮狀態(tài)空間分析，但是自動化程度不高，需要人工干預(yù)，并且在證明失敗后不能給出易于理解的反例。本文使用符號模型檢查技術(shù)來驗證嵌入式軟件系統(tǒng)，并通過觸摸屏檢測算法來說明該方法的應(yīng)用。
　　1 模型檢查
　　模型檢查是一種驗證有限狀態(tài)系統(tǒng)的自動化技術(shù)，使用時序邏輯來描述系統(tǒng)性質(zhì)。本文使用時序邏輯CTL來描述嵌入式系統(tǒng)滿足的性質(zhì)。CTL有分支時間和線性時間2種算子，其中分支時間算子是指路徑量詞A（“對所有計算路徑”）和E（“對某些計算路徑”），線性時間算子包括G（“always”，總是）、F（“somet：imes”，有時）、X（“next-time”，下一時刻）和U（“until”，直到）。其中線性時間算子G、F、X和U之前必須有1個路徑量詞。如圖1所示，CTL公式用于描述有限狀態(tài)系統(tǒng)上計算路徑的相關(guān)性質(zhì)。圖1（a）表示EFg，即“存在一條計算路徑，在某個狀態(tài)，布爾量公式g為真”；圖1（b）表示AFg，即“對所有計算路徑，在每個計算路徑的某個狀態(tài)，布爾量公式g為真”；圖1（c）表示EG，即“存在一條計算路徑，在此路徑的所有狀態(tài)，布爾量公式g為真”；圖1（d）表示AG，即“在所有計算路徑的所有狀態(tài)，布爾量公式g都為真”。
　　
2 模型檢查工具SMV
　　常見的模型檢查工具有貝爾實驗室開發(fā)的SPIN、赫爾辛基工業(yè)大學(xué)計算機(jī)理論實驗室開發(fā)的PR（）D和MA—RIA、美國CMU計算機(jī)學(xué)院開發(fā)的SMV等。本文使用SMV作為對嵌入式軟件驗證的模型檢查工具。
　　SMV基于“符號模型檢查”（Symbolic Model Claec-king）技術(shù)，開始是為了研究符號模型檢查應(yīng)用的可能性而開發(fā)的一種對硬件進(jìn)行檢查的實驗工具，現(xiàn)在已經(jīng)發(fā)展成為廣為流行的分析有限狀態(tài)系統(tǒng)的常用工具。
　　本文中，軟件系統(tǒng)模型用SMV語言描述。1個SMV程序由2部分組成：1個有限狀態(tài)轉(zhuǎn)換系統(tǒng)和1組CTL公式。SMV把初始狀態(tài)和轉(zhuǎn)換關(guān)系表示成二叉樹圖BDD（Binary Deciding Diagram），CTL公式表示系統(tǒng)模型的屬性，也表示成BDD。通過模型檢查算法遍歷系統(tǒng)狀態(tài)空間，給出1個聲明的屬性是正確或者不正確的驗證結(jié)果，并給出1個不滿足該屬性的反例。1個CTL公式真正的值通過遍歷狀態(tài)圖的方式確定，這種遍歷的時間復(fù)雜性和狀態(tài)空間大小、公式的長度成線性關(guān)系。
　　3 觸摸屏檢測軟件代碼的驗證
　　觸摸屏作為人機(jī)界面的輸入設(shè)備已經(jīng)廣泛應(yīng)用于各種嵌入式系統(tǒng)中，如手持設(shè)備、工業(yè)控制、車載設(shè)備等。對于有些應(yīng)用，觸摸屏是關(guān)鍵的輸入設(shè)備，觸摸屏失效會導(dǎo)致整個系統(tǒng)不可用。因此設(shè)計高效、清晰、可靠的觸摸屏驅(qū)動程序非常重要。本文使用有限狀態(tài)機(jī)來描述觸摸屏檢測算法，然后使用SMV語言來描述此有限狀態(tài)系統(tǒng)模型，最后使用SMV工具對此模型進(jìn)行驗證。