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

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

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

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