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

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

上述語言描述中，模塊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í)，表示觸筆沒有按下，為0時(shí)表示有觸筆按下中斷；d_jittery_delay為1表示觸筆按下消抖時(shí)間到；u_jittery_delay表示觸筆抬起消抖時(shí)間到。
本文主要驗(yàn)證了觸摸屏檢測(cè)狀態(tài)機(jī)的可達(dá)屬性。屬性用公式(1)和(2)描述。公式(1)的含義是，從檢測(cè)狀態(tài)為抬起并其觸筆無按下開始的所有計(jì)算路徑中，總存在1條計(jì)算路徑，能夠到達(dá)檢測(cè)狀態(tài)為按下。公式(2)的含義是，從檢測(cè)狀態(tài)為按下并其觸筆為按下開始的所有計(jì)算路徑中，總存在1條計(jì)算路徑，能夠到達(dá)檢測(cè)狀態(tài)為抬起。
3．3 驗(yàn)證結(jié)果
在Intel CPU
通過這個(gè)驗(yàn)證結(jié)果，可知3．2節(jié)中描述的觸摸屏檢測(cè)算法模型滿足狀態(tài)可達(dá)性。

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