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

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

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