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

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

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