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

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

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

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

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

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

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

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

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

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