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

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

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