模型檢驗(yàn)狀態(tài)空間縮減技術(shù)研究及輔助工具的設(shè)計(jì).pdf

1、模型檢驗(yàn)是一種基于對(duì)系統(tǒng)的狀態(tài)空間進(jìn)行窮舉搜索的自動(dòng)驗(yàn)證技術(shù)。對(duì)并發(fā)和實(shí)時(shí)系統(tǒng)進(jìn)行模型檢驗(yàn)時(shí),狀態(tài)數(shù)目往往隨著并發(fā)分量和系統(tǒng)中無(wú)窮的時(shí)間值數(shù)目的增加呈指數(shù)增長(zhǎng)；因此,當(dāng)實(shí)時(shí)系統(tǒng)的并發(fā)數(shù)量較多時(shí),直接對(duì)其狀態(tài)空間進(jìn)行窮舉搜索是不可行的,這就是所謂的狀態(tài)爆炸問(wèn)題。隨著模型檢驗(yàn)技術(shù)在各個(gè)領(lǐng)域的深入應(yīng)用,狀態(tài)爆炸問(wèn)題日益成為其廣泛應(yīng)用道路上的最大障礙,如何縮減狀態(tài)空間避免狀態(tài)爆炸已經(jīng)成為模型檢驗(yàn)技術(shù)亟待研究的一個(gè)重要課題。有鑒于此,我們進(jìn)行了關(guān)

2、于模型檢驗(yàn)狀態(tài)空間縮減技術(shù)方面的研究。
　　 本文首先探討了模型檢驗(yàn)的一般過(guò)程及其框架,接著簡(jiǎn)單介紹了已有的模型檢驗(yàn)工具，在此基礎(chǔ)上詳細(xì)地分析了狀態(tài)爆炸問(wèn)題產(chǎn)生的因?yàn)?為新模型的建立和狀態(tài)的表示奠定了必要的基礎(chǔ)，最后詳細(xì)討論了縮減模型檢驗(yàn)狀態(tài)空間的技術(shù)和實(shí)現(xiàn)方法。狀態(tài)空間的大小和系統(tǒng)的模型、模型的形式化表示和公式的形式化表示有著非常密切的關(guān)系；因此,在馬爾可夫鏈和二元決策圖的基礎(chǔ)上,引入了模糊馬爾可夫鏈,用MTBDD來(lái)對(duì)系統(tǒng)模型