一種基于模型檢查的嵌入式軟件驗證方法

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

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

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