基于SAT的有界模型檢測(cè)及其應(yīng)用研究.pdf

1、無論在計(jì)算機(jī)系統(tǒng)硬件設(shè)計(jì)方面還是在軟件設(shè)計(jì)方面，隨著設(shè)計(jì)規(guī)模越來越復(fù)雜和龐大，會(huì)產(chǎn)生越來越多的設(shè)計(jì)缺陷和錯(cuò)誤等。用一些傳統(tǒng)的方法往往是代價(jià)很高，但還難以檢測(cè)出它們。形式化驗(yàn)證的優(yōu)點(diǎn)是在一個(gè)設(shè)計(jì)或系統(tǒng)的研制周期的前期進(jìn)行。在研制周期的早期進(jìn)行分析和驗(yàn)證，可大大降低返工的成本，提高效率?；谶@些原因，有界模型檢測(cè)(Bounded Model Checking簡(jiǎn)稱BMC)作為一種重要的形式化驗(yàn)證的方法，它的相關(guān)技術(shù)的研究和應(yīng)用在當(dāng)前具有相當(dāng)重

2、要的價(jià)值和意義。 有界模型檢測(cè)是通過把有限狀態(tài)機(jī)(FSM)和LTL邏輯驗(yàn)證規(guī)范否定形式編碼成SAT實(shí)例，再由各種SAT工具來求解，以獲得反例。該方法相比基于OBDD技術(shù)的模型檢測(cè)，進(jìn)一步減輕的狀態(tài)空間爆炸問題，且給出的反例是最短的。 因?yàn)锽MC較晚出現(xiàn)，它的很多相關(guān)的技術(shù)不完善、相關(guān)的應(yīng)用也不普遍。本文圍繞BMC的相關(guān)技術(shù)和應(yīng)用進(jìn)行了一定的研究。主要工作如下： BMC編碼技術(shù)的優(yōu)化可生成規(guī)模小易于求解的SAT實(shí)例

3、，對(duì)提高有界模型檢測(cè)的效率至關(guān)重要，近年其是BMC研究中一個(gè)熱點(diǎn)問題。本文結(jié)合FSM狀態(tài)轉(zhuǎn)移的特性和線性時(shí)序邏輯的語義，在現(xiàn)有的編碼基礎(chǔ)上，對(duì)有界模型檢測(cè)中對(duì)驗(yàn)證G(p)和G(p→F(q))這兩個(gè)很重要很常用的模態(tài)算子轉(zhuǎn)換公式進(jìn)行了優(yōu)化，給出了簡(jiǎn)潔高效的遞推公式；證明了遞推公式和原公式的邏輯關(guān)系；基于遞推公式設(shè)計(jì)了編碼算法。通過實(shí)驗(yàn)比較分析，基于遞推公式編碼算法在生成SAT實(shí)例規(guī)模和求解效率方面，都優(yōu)于現(xiàn)有的兩個(gè)主流的編碼算法。所給出的

4、方法和思想對(duì)有界模型檢測(cè)的其他模態(tài)算子編碼的優(yōu)化，有直接的參考價(jià)值。 SAT工具是BMC的后端求解工具。SAT問題的研究對(duì)包括BMC在內(nèi)的許多領(lǐng)域都很有意義。局部搜索方法是求解SAT實(shí)例的一類重要的方法。本文提出用初始概率的方法對(duì)局部搜索算法中的變量的初始隨機(jī)指派進(jìn)行適當(dāng)?shù)募s束，用該方法對(duì)目前的一些重要的SAT問題的局部搜索算法進(jìn)行改進(jìn)，通過對(duì)不同結(jié)構(gòu)、不同規(guī)模的SAT問題的實(shí)例測(cè)試表明，改進(jìn)后的這些局部搜索算法的效率有了較大的