<dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><s id="yhprb"><strike id="yhprb"></strike></s></dfn><small id="yhprb"></small><dfn id="yhprb"></dfn><small id="yhprb"><delect id="yhprb"></delect></small><small id="yhprb"></small><small id="yhprb"></small> <delect id="yhprb"><strike id="yhprb"></strike></delect><dfn id="yhprb"></dfn><dfn id="yhprb"></dfn><s id="yhprb"><noframes id="yhprb"><small id="yhprb"><dfn id="yhprb"></dfn></small><dfn id="yhprb"><delect id="yhprb"></delect></dfn><small id="yhprb"></small><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn> <small id="yhprb"></small><delect id="yhprb"><strike id="yhprb"></strike></delect><dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"><s id="yhprb"><strike id="yhprb"></strike></s></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn>

新聞中心

EEPW首頁(yè) > 嵌入式系統 > 設計應用 > 一種基于模型檢查的嵌入式軟件驗證方法

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

作者: 時(shí)間:2009-07-02 來(lái)源:網(wǎng)絡(luò ) 收藏

廣泛應用于不同領(lǐng)域,如消費電子、工業(yè)控制、汽車(chē)電子、移動(dòng)通信等。的可靠性保證十分關(guān)鍵。中常見(jiàn)的錯誤包括狀態(tài)機錯誤、時(shí)序錯誤、棧溢出/存儲溢出等,在開(kāi)發(fā)過(guò)程中對嵌入式軟件進(jìn)行十分重要。
對嵌入式軟件的一般依賴(lài)于形式化的。
形式化的可以對嵌入式軟件系統進(jìn)行嚴格的規約,并可以對系統進(jìn)行不同視角的。驗證主要是分析系統是否具有期望的性質(zhì)。常見(jiàn)的驗證技術(shù)主要有和定理證明。自動(dòng)化程度高,并且當系統不具有期望性質(zhì)時(shí)能給出反例,但它存在狀態(tài)爆炸問(wèn)題。定理證明能無(wú)窮狀態(tài)空間分析,但是自動(dòng)化程度不高,需要人工干預,并且在證明失敗后不能給出易于理解的反例。本文使用符號技術(shù)來(lái)驗證嵌入式軟件系統,并通過(guò)觸摸屏檢測算法來(lái)說(shuō)明該的應用。

本文引用地址:http://dyxdggzs.com/article/152441.htm


1 模型檢查
模型檢查是一種驗證有限狀態(tài)系統的自動(dòng)化技術(shù),使用時(shí)序邏輯來(lái)描述系統性質(zhì)。本文使用時(shí)序邏輯CTL來(lái)描述嵌入式系統滿(mǎn)足的性質(zhì)。CTL有分支時(shí)間和線(xiàn)性時(shí)間2種算子,其中分支時(shí)間算子是指路徑量詞A(“對所有計算路徑”)和E(“對某些計算路徑”),線(xiàn)性時(shí)間算子包括G(“always”,總是)、F(“somet:imes”,有時(shí))、X(“next-time”,下一時(shí)刻)和U(“until”,直到)。其中線(xiàn)性時(shí)間算子G、F、X和U之前必須有1個(gè)路徑量詞。如圖1所示,CTL公式用于描述有限狀態(tài)系統上計算路徑的相關(guān)性質(zhì)。圖1(a)表示EFg,即“存在一條計算路徑,在某個(gè)狀態(tài),布爾量公式g為真”;圖1(b)表示AFg,即“對所有計算路徑,在每個(gè)計算路徑的某個(gè)狀態(tài),布爾量公式g為真”;圖1(c)表示EG,即“存在一條計算路徑,在此路徑的所有狀態(tài),布爾量公式g為真”;圖1(d)表示AG,即“在所有計算路徑的所有狀態(tài),布爾量公式g都為真”。

2 模型檢查工具SMV
常見(jiàn)的模型檢查工具有貝爾實(shí)驗室開(kāi)發(fā)的SPIN、赫爾辛基工業(yè)大學(xué)計算機理論實(shí)驗室開(kāi)發(fā)的PR()D和MA―RIA、美國CMU計算機學(xué)院開(kāi)發(fā)的SMV等。本文使用SMV作為對嵌入式軟件驗證的模型檢查工具。
SMV“符號模型檢查”(Symbolic Model Claec-king)技術(shù),開(kāi)始是為了研究符號模型檢查應用的可能性而開(kāi)發(fā)的一種對硬件進(jìn)行檢查的實(shí)驗工具,現在已經(jīng)發(fā)展成為廣為流行的分析有限狀態(tài)系統的常用工具。
本文中,軟件系統模型用SMV語(yǔ)言描述。1個(gè)SMV程序由2部分組成:1個(gè)有限狀態(tài)轉換系統和1組CTL公式。SMV把初始狀態(tài)和轉換關(guān)系表示成二叉樹(shù)圖BDD(Binary Deciding Diagram),CTL公式表示系統模型的屬性,也表示成BDD。通過(guò)模型檢查算法遍歷系統狀態(tài)空間,給出1個(gè)聲明的屬性是正確或者不正確的驗證結果,并給出1個(gè)不滿(mǎn)足該屬性的反例。1個(gè)CTL公式真正的值通過(guò)遍歷狀態(tài)圖的方式確定,這種遍歷的時(shí)間復雜性和狀態(tài)空間大小、公式的長(cháng)度成線(xiàn)性關(guān)系。


3 觸摸屏檢測軟件代碼的驗證
觸摸屏作為人機界面的輸入設備已經(jīng)廣泛應用于各種嵌入式系統中,如手持設備、工業(yè)控制、車(chē)載設備等。對于有些應用,觸摸屏是關(guān)鍵的輸入設備,觸摸屏失效會(huì )導致整個(gè)系統不可用。因此設計高效、清晰、可靠的觸摸屏驅動(dòng)程序非常重要。本文使用有限狀態(tài)機來(lái)描述觸摸屏檢測算法,然后使用SMV語(yǔ)言來(lái)描述此有限狀態(tài)系統模型,最后使用SMV工具對此模型進(jìn)行驗證。
3.1 觸摸屏檢測的有限狀態(tài)機
本文為了描述的簡(jiǎn)單,簡(jiǎn)化了觸摸屏檢測的過(guò)程。如圖2所示,將觸摸屏檢測分為5個(gè)狀態(tài):觸摸屏空閑(Tou-ch-Idle)、觸摸屏抬起狀態(tài)(Touch_Up)、觸摸屏按下檢測狀態(tài)(Touch_ChkDown)、觸摸屏按下?tīng)顟B(tài)(Touch_Down)以及觸摸屏抬起檢測狀態(tài)(Touch_ChkUp)。觸摸屏狀態(tài)機是由事件觸發(fā)來(lái)進(jìn)行狀態(tài)變換的,觸發(fā)事件有觸筆按下中斷、觸筆按下消抖定時(shí)溢出、觸筆抬起中斷、觸筆抬起消抖定時(shí)溢出。

linux操作系統文章專(zhuān)題:linux操作系統詳解(linux不再難懂)

超級電容器相關(guān)文章:超級電容器原理



上一頁(yè) 1 2 下一頁(yè)

評論


相關(guān)推薦

技術(shù)專(zhuān)區

關(guān)閉
国产精品自在自线亚洲|国产精品无圣光一区二区|国产日产欧洲无码视频|久久久一本精品99久久K精品66|欧美人与动牲交片免费播放
<dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><s id="yhprb"><strike id="yhprb"></strike></s></dfn><small id="yhprb"></small><dfn id="yhprb"></dfn><small id="yhprb"><delect id="yhprb"></delect></small><small id="yhprb"></small><small id="yhprb"></small> <delect id="yhprb"><strike id="yhprb"></strike></delect><dfn id="yhprb"></dfn><dfn id="yhprb"></dfn><s id="yhprb"><noframes id="yhprb"><small id="yhprb"><dfn id="yhprb"></dfn></small><dfn id="yhprb"><delect id="yhprb"></delect></dfn><small id="yhprb"></small><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn> <small id="yhprb"></small><delect id="yhprb"><strike id="yhprb"></strike></delect><dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"><s id="yhprb"><strike id="yhprb"></strike></s></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn>