基于SAT的符號化模型檢驗技術(shù)研究.pdf

1、隨著計算機(jī)技術(shù)的不斷進(jìn)步，計算機(jī)系統(tǒng)的軟硬件設(shè)計越來越復(fù)雜，過于復(fù)雜和龐大的設(shè)計必定會帶來越來越多的設(shè)計缺陷和錯誤。傳統(tǒng)的方法很難檢測到系統(tǒng)設(shè)計中的所有錯誤。然而，系統(tǒng)的安全性在航空、航天、國防、醫(yī)療等安全攸關(guān)的領(lǐng)域卻非常重要。因此，用以保證系統(tǒng)正確性的形式化方法亟待出現(xiàn)。
　　模型檢驗是上世紀(jì)80年代提出的一種針對有窮狀態(tài)系統(tǒng)進(jìn)行自動化驗證的技術(shù)。經(jīng)過30多年的發(fā)展，模型檢驗技術(shù)已經(jīng)是計算機(jī)輔助驗證領(lǐng)域非常重要的技術(shù)之一。然而，

2、狀態(tài)空間爆炸問題始終是制約模型檢驗技術(shù)發(fā)展的最大障礙。為此，研究人員提出了很多技術(shù)來對付該問題，比如基于BDD的符號化模型檢驗技術(shù)、偏序歸約技術(shù)、抽象精化技術(shù)等。近年來，隨著SAT技術(shù)的進(jìn)展，Biere[1]等人提出了基于SAT的限界模型檢驗技術(shù)。該技術(shù)利用SAT求解器的能力進(jìn)一步提高了模型檢驗技術(shù)處理問題的規(guī)模。目前，基于SAT的符號化模型檢驗技術(shù)已經(jīng)成為計算機(jī)輔助驗證領(lǐng)域研究的熱點問題之一。
　　然而，在實際應(yīng)用中，基于SAT

3、的符號化驗證技術(shù)還存在諸多問題，比如驗證效率、驗證能力、完全性等。本文圍繞基于SAT的符號化模型檢驗技術(shù)進(jìn)行了一系列研究，旨在進(jìn)一步提高該技術(shù)的效率以及擴(kuò)展該技術(shù)處理問題的能力。
　　本文的主要貢獻(xiàn)包括：
　　1）優(yōu)化了LTL的限界模型檢驗技術(shù)
　　針對現(xiàn)有的LTL的限界模型檢驗技術(shù)，本文提出兩種優(yōu)化的方法。第一種優(yōu)化技術(shù)是一種稱為反例集合保持的化簡技術(shù)，該技術(shù)的核心思想就是在進(jìn)行模型檢驗之前，首先使用一種輕量級的技術(shù)

4、對待驗證的LTL性質(zhì)進(jìn)行化簡，使得化簡后的性質(zhì)與原性質(zhì)關(guān)于待驗證的模型是等價的。因此，在真正的模型檢驗中，就可以使用化簡后的性質(zhì)代替原性質(zhì)進(jìn)行驗證，該技術(shù)對于復(fù)雜的性質(zhì)規(guī)約具有非常明顯的作用。第二種優(yōu)化技術(shù)，是利用SAT求解器的增量式求解能力，優(yōu)化了基于語義的限界模型檢驗編碼，實驗表明，新的編碼在驗證效率上，相對于其他編碼有很大的優(yōu)勢。這兩種技術(shù)可以很自然地結(jié)合起來，從而提高LTL的限界模型檢驗效率。
　　2）提出ω-正規(guī)性質(zhì)的限

5、界模型檢驗算法。
　　由于在工業(yè)應(yīng)用中，許多重要的時序性質(zhì)無法采用LTL表達(dá)，因此，針對ω-正規(guī)性質(zhì)的限界模型檢驗具有十分重要的理論和實際意義。本文針對兩種具有ω-正規(guī)表達(dá)能力的時序邏輯ETLl+f和QTL，分別提出了對應(yīng)的限界模型檢驗算法。針對ETLl+f，本文提出了基于語義的限界模型檢驗算法。該技術(shù)的核心是構(gòu)造ETLl+f的tableau，通過擴(kuò)展LTL的tableau構(gòu)造技術(shù)，本文提出了ETLl+f的tableau構(gòu)造算法。

6、針對QTL，本文提出了兩種限界模型檢驗算法，分別為基于語法的限界模型檢驗和基于語義的限界模型檢驗?；谡Z法的限界模型檢驗的核心思想是將QTL公式的限界語義編碼成QBF公式，然后利用QBF求解器來驗證該問題?；谡Z義的限界模型檢驗同樣是通過擴(kuò)展LTL的tableau構(gòu)造方法得到QTL的tableau構(gòu)造方法，然后將限界模型檢驗問題轉(zhuǎn)化為受限路徑上的公平性路徑查找問題。然后，將公平性路徑查找問題編碼成布爾公式，最后利用SAT求解器來驗證該問

7、題。
　　3）提出了基于SAT的符號化模型檢驗的完全性保證的算法。
　　制約限界模型檢驗技術(shù)應(yīng)用的一個主要瓶頸在于其不是一種完全的技術(shù)，即它不能證明給定的模型是否滿足給定的性質(zhì)。然而，線性時序邏輯的模型檢驗問題最終都可以轉(zhuǎn)化為公平性路徑查找問題，而公平性路徑查找問題可以轉(zhuǎn)化為若干個可達(dá)性問題。因此，開發(fā)高效的可達(dá)性算法是解決基于SAT符號化模型檢驗完全性保證技術(shù)的核心。本文基于目前最好的可達(dá)性算法，即屬性指導(dǎo)的可達(dá)性分析算法

8、（Property Directed Reachability，簡稱PDR），提出了兩種新的可達(dá)性算法。兩種算法的核心思想都是試圖通過雙向逼近可達(dá)狀態(tài)空間，從而加快算法的收斂速度。實驗結(jié)果表明，本文提出的可達(dá)性算法相對于基本的算法有了很大的提高。
　　4）實現(xiàn)了兩個實用的工具。
　　模型檢驗技術(shù)的最終目的是應(yīng)用，將理論上的算法轉(zhuǎn)化為實用的工具是模型檢驗技術(shù)非常重要的一部分。本文實現(xiàn)了兩個實用工具，分別支持本文提出的各個算法。

9、工具ENuSMV是基于開源的符號化模型檢驗工具NuSMV實現(xiàn)的，它支持本文提出的C?PR?（Counter?xample Preserving R?duction，簡稱C?PR?）算法、增量式的基于語義的LTL限界模型檢驗算法、基于語義的ETLl+f的限界模型檢驗算法。工具Reach是一個全新的基于SAT的符號化模型檢驗工具，它不僅支持本文提出的交疊的PDR算法以及并行的PDR算法，還支持其他著名的可達(dá)性算法，包括限界模型檢驗算法、k步