SPIN模型檢測的形式化分析機理研究及應(yīng)用.pdf

1、隨著計算機軟硬件系統(tǒng)日益復(fù)雜，如何保證其正確性和可靠性成為日益緊迫的問題。確保這些系統(tǒng)的可靠性成為計算機科學(xué)領(lǐng)域中重要研究領(lǐng)域。為此提出的諸多方法和理論中，模型檢測以其簡潔明了和自動化程度高而倍受注目。模型檢測是一種重要的形式化自動驗證技術(shù)，此技術(shù)的成功應(yīng)用歸功于有效驗證工具的開發(fā)和支持。SPIN是一種著名的分析驗證并發(fā)系統(tǒng)邏輯一致性的模型檢測工具。模型檢測的瓶頸問題是狀態(tài)爆炸問題，如何以使用精簡方式描述系統(tǒng)，避免因為模型復(fù)雜而引起狀態(tài)

2、爆炸是一個值得研究的方向。 本文在闡述SPIN模型檢測形式化分析機理及線性時態(tài)邏輯LTL性質(zhì)的基礎(chǔ)上，詳細分析了基于SPIN的系統(tǒng)建模語言Promela中的并發(fā)進程、通道操作、基本數(shù)據(jù)結(jié)構(gòu)及其功能，設(shè)計了模型檢測求解離散化問題的方法--通過Promela建立模型，在描述系統(tǒng)屬性(性質(zhì))中運用分支界限技術(shù)，驗證過程中LTL公式動態(tài)變化，旨在減少模型狀態(tài)空間，提高搜索效率，實例分析驗證了此方法的正確性；同時采用了啟發(fā)式策略優(yōu)化模型，