符號(hào)模型檢測(cè)的研究.pdf

1、計(jì)算機(jī)軟硬件系統(tǒng)日益復(fù)雜,在很多系統(tǒng)中,測(cè)試、模擬等傳統(tǒng)的驗(yàn)證方法已不能保證其正確性和可靠性。模型檢測(cè)技術(shù)產(chǎn)生于上世紀(jì)80年代,由美國(guó)的Clarke和Emerson,法國(guó)的Quielle和Sifakis分別獨(dú)立提出。在該形式化驗(yàn)證方法中,系統(tǒng)性質(zhì)用命題時(shí)態(tài)邏輯公式表示,有限狀態(tài)反應(yīng)系統(tǒng)(硬件電路、通訊協(xié)議)用狀態(tài)轉(zhuǎn)換系統(tǒng)描述,有效的查詢過(guò)程檢測(cè)模型,判斷模型是否滿足系統(tǒng)性質(zhì)。然而,隨著系統(tǒng)規(guī)模的增大,狀態(tài)數(shù)呈指數(shù)上升的狀況和顯式模型檢測(cè)

2、有限的處理能力之間存在難以克服的矛盾,即狀態(tài)爆炸。1986年,Bryant將傳統(tǒng)的二值判定圖BDD技術(shù)加以改進(jìn),使之成為布爾函數(shù)的規(guī)范表示方法。之后McMillan將這種技術(shù)應(yīng)用于模型檢測(cè)中,基于BDD的模型檢測(cè)稱為符號(hào)模型檢測(cè)。符號(hào)模型檢測(cè)的主要特點(diǎn)是用BDD隱式地表示有限狀態(tài)反應(yīng)系統(tǒng)的狀態(tài)集合和狀態(tài)轉(zhuǎn)換集合,空間爆炸問(wèn)題被有效緩解。 本研究實(shí)現(xiàn)了一個(gè)基本的符號(hào)模型檢測(cè)器CTLMC。該模型檢測(cè)器直接采用布爾函數(shù)作為系統(tǒng)模型的描

3、述語(yǔ)言,用來(lái)描述模型的初始狀態(tài)集合和系統(tǒng)狀態(tài)轉(zhuǎn)換關(guān)系；采用CTL時(shí)態(tài)邏輯作為系統(tǒng)性質(zhì)的描述語(yǔ)言,用來(lái)描述系統(tǒng)應(yīng)該滿足的需求(性質(zhì));采用CTL符號(hào)模型檢測(cè)算法計(jì)算模型是否滿足性質(zhì)。 此外,在實(shí)現(xiàn)CTLMC過(guò)程中發(fā)現(xiàn)一種基于BDD的SMC中PRE3操作的改進(jìn)算法,該算法處理PRE3步驟3(嵌套布爾存在量化)的方法是,一次遍歷“刪除”所有被量化變量的節(jié)點(diǎn),產(chǎn)生表示布爾函數(shù)與嵌套存在量化結(jié)果等價(jià)的不確定排序二值判定圖,然后把不確定排序