基于寬度優(yōu)先搜索的模型檢測技術(shù)研究.pdf

1、模型檢測技術(shù)是一種非常重要的形式化驗證技術(shù)，其最大的優(yōu)點就是全自動進(jìn)行驗證。模型檢測技術(shù)已被應(yīng)用于計算機(jī)硬件、通信協(xié)議、控制系統(tǒng)、安全認(rèn)證協(xié)議等方面的分析與驗證中，取得了令人矚目的成就，并從學(xué)術(shù)界輻射到了工業(yè)界。但是，模型檢測過程中的狀態(tài)空間爆炸問題嚴(yán)重制約著模型檢測技術(shù)在工業(yè)界的應(yīng)用。
　　本文以此為背景，對模型檢測技術(shù)的相關(guān)理論知識進(jìn)行了學(xué)習(xí)分析，包括時態(tài)邏輯、自動機(jī)和模型檢測算法。圍繞基于磁盤的BFS寬度優(yōu)先搜索模型檢測技術(shù)

2、，重點分析研究了模型檢測過程中的延遲重復(fù)檢測，主要內(nèi)容為：
　　1、研究模型檢測過程中狀態(tài)空間搜索時的延遲重復(fù)檢測，提出了一種基于分區(qū)的延遲重復(fù)檢測方法。該方法針對BFS寬度優(yōu)先搜索出現(xiàn)的某些層所擁有的狀態(tài)無法全部存儲到內(nèi)存中，而影響了模型檢測的進(jìn)行，將每一層的狀態(tài)進(jìn)行分區(qū)劃分，以適應(yīng)內(nèi)存的限制，提高了模型檢測的時間性能。
　　2、研究有限狀態(tài)系統(tǒng)狀態(tài)轉(zhuǎn)移局部性的統(tǒng)計特性，提出了將這一統(tǒng)計特性應(yīng)用于上述基于分區(qū)的延遲重復(fù)檢測