模型檢測形式化分析中若干關(guān)鍵問題研究.pdf

1、模型檢測是近二十年來最成功的形式化自動(dòng)驗(yàn)證技術(shù)之一。其因自動(dòng)化程度高，效率高等優(yōu)點(diǎn)而被廣泛應(yīng)用于并發(fā)系統(tǒng)的分析與驗(yàn)證中。與定理證明等其他形式化驗(yàn)證方法相比，模型檢測的主要優(yōu)點(diǎn)在于：當(dāng)斷言被違反時(shí)，模型檢測方法能夠給出反例，以解釋斷言被違反的原因。然而，由于復(fù)雜系統(tǒng)的反例通常很長，導(dǎo)致非常難以理解，需要花費(fèi)大量時(shí)間檢查大量的變量和事件，才能夠找到錯(cuò)誤的根源。這些客觀因素都影響了模型檢測驗(yàn)證的效率。狀態(tài)爆炸問題一直是模型檢測的瓶頸問題。為了

2、能夠有效地應(yīng)用模型檢測方法，研究人員提出可以減少和壓縮狀態(tài)空間以緩解狀態(tài)爆炸問題。 因此，論文主要從模型檢測的反例最小化分析、解決狀態(tài)爆炸問題以及擴(kuò)充Promela三個(gè)方面進(jìn)行了研究，具體內(nèi)容如下： 1、介紹了Gastin.P最小反例算法思想，結(jié)合著名的Needham-Schroeder公鑰身份認(rèn)證協(xié)議對(duì)算法進(jìn)行了非形式化分析，實(shí)例分析的結(jié)果表明了算法的有效性。在算法的基礎(chǔ)上結(jié)合語法重定序策略提出了一種新的算法框架，解決