符號模型檢測的研究.pdf

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

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

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