于露

摘要：無論是計算機系統(tǒng)硬件設(shè)計還是軟件設(shè)計，隨著設(shè)計規(guī)模越來越復(fù)雜和龐大，會產(chǎn)生越來越多的設(shè)計缺陷。傳統(tǒng)檢測方法代價高，并且難以檢測這些設(shè)計缺陷。有界模型檢驗是一種重要的形式化驗證方法，可以大大提高檢測、驗證的效率。作為一種形式化方法構(gòu)造系統(tǒng)的模擬運行過程，有界模型檢驗通過把有限狀態(tài)機和線性時序邏輯驗證規(guī)范否定形式編碼成布爾可滿足性實例，再由各種布爾可滿足性工具來求解，以獲得反例。由于有界模型檢驗使用深度優(yōu)先搜索，它可以很快找到路徑最短的反例。

關(guān)鍵詞：有界模型檢驗；模型檢驗；SAT

中圖分類號：TP311 文獻標(biāo)識碼：A 文章編號：1009-3044（2017）35-0070-02

1 有界模型檢驗的概念

模型檢測（model checking）是形式化驗證方法的一種，它可以自動檢測系統(tǒng)的模擬運行是否滿足某些期望的規(guī)范。隨著計算機系統(tǒng)越來越復(fù)雜，網(wǎng)絡(luò)應(yīng)用越來越普及和重要，通過模型檢測技術(shù)來驗證系統(tǒng)和網(wǎng)絡(luò)的安全性和正確性的應(yīng)用也逐漸增多。針對前期的OBDD（ordered binary decision diagram）技術(shù)的模型檢測的不足，有界模型檢測（bounded model checking，簡稱BMC）使用SAT（satisfiability）求解器來求解

需要驗證的問題。BMC通過設(shè)置界限閾值k，可以有效地克服狀態(tài)爆炸問題，并可以解決邏輯公式相對應(yīng)的BDD（binary decision diagram）結(jié)構(gòu)的存儲空間、檢測變量少等問題[1]。BMC有兩個主要的優(yōu)勢：其優(yōu)勢之一是充分利用SAT（satisfiability）求解工具的特征，把BMC 問題編碼成SAT實例，有效地使模型檢驗的變量數(shù)提升一個數(shù)量級以上；另一優(yōu)勢是BMC的求解過程向著不滿足命題的方向發(fā)展，有利于得到長度最短、最簡明的反例，方便設(shè)計者理解問題，找出原因。實驗驗證，當(dāng)邊界閾值的上界k小于60時，BMC優(yōu)于傳統(tǒng)的模型檢測[2]。

2 有界模型檢驗的過程

有界模型檢測的主要過程是：使用有限狀態(tài)自動機（finite state machine，F(xiàn)SM）來表示要驗證的模型或系統(tǒng)，通過FSM狀態(tài)間的轉(zhuǎn)移來模擬系統(tǒng)或模型運行；用線性時序邏輯（linear-time temporal logic，LTL）來描述有限狀態(tài)自動機；設(shè)定邊界閾值k；FSM 狀態(tài)間的轉(zhuǎn)移關(guān)系和LTL邏輯規(guī)范使用邏輯與來構(gòu)成BMC轉(zhuǎn)換公式；把BMC轉(zhuǎn)換公式編碼成SAT實例，借助SAT工具求解。若有解，則產(chǎn)生反例反之，若無解，則系統(tǒng)一直運行到閾值k階段后停止，說明系統(tǒng)或模型是安全且沒有錯誤的。

2.1 Kripke結(jié)構(gòu)

有限狀態(tài)機可以被表示成kripke結(jié)構(gòu)。

Kripke結(jié)構(gòu)由狀態(tài)集、狀態(tài)之間的轉(zhuǎn)移關(guān)系、每個狀態(tài)上使一組原子命題為真的集合組成[3]。它的定義為：

定義一：設(shè)AP是一組原子命題，AP上的一個Kripke結(jié)構(gòu)M定義為四元組M=（S，S0，R，L），其中：

1） S是一個有限狀態(tài)集合；

2） S0 ? S 是初始狀態(tài)集合；

3） R ? S×S 是轉(zhuǎn)移關(guān)系，要求是完全的，即對?s∈S都存在一個狀態(tài)?s‘∈S，使得（s，s）∈R成立；

4） L：S→2AP是一個函數(shù)，標(biāo)記每個狀態(tài)使某些原子命題為真的函數(shù)。

在Kripke結(jié)構(gòu)中，從一個狀態(tài)s開始的一條路徑是一個無限狀態(tài)序列，π=s0s1…，其中s0=s且R（si，si+1）對所有i≥0成立。

Kripke結(jié)構(gòu)是一種數(shù)學(xué)結(jié)構(gòu)，目前在模型檢驗上是用比較多，可以表示為狀態(tài)圖。它可以用命題語句來表示狀態(tài)之間的轉(zhuǎn)移關(guān)系。使用Kripke結(jié)構(gòu)來進行證明的優(yōu)勢是：

1） 可以反映程序執(zhí)行的狀態(tài)；

2） 程序的執(zhí)行過程可以由狀態(tài)圖來表示。

2.2 線性時序邏輯

線性時序邏輯是經(jīng)典邏輯的延伸，它繼承了布爾變量和布爾操作，類如﹁非運算、∧與運算、→條件運算等。除了布爾連接符，LTL還有如下時序修飾符：

1） X（next）：下一個；

2） G（globally）：總是；

3） F（future）：未來；

4） U（until）：直到；

5） R（release）：釋放。

線性時序邏輯將有限狀態(tài)機各個狀態(tài)之間的邏輯用符號表示出來。BMC通過對各個狀態(tài)的布爾值進行對比，來判斷是否滿足屬性。

2.3 屬性的分類

BMC的屬性分為兩種：安全屬性和活力屬性[4]。前者聲明什么狀態(tài)不應(yīng)該發(fā)生，換句話說也就是什么狀態(tài)應(yīng)該發(fā)生；后者聲明什么狀態(tài)最終應(yīng)該發(fā)生。安全屬性的反例為一個狀態(tài)蹤跡，這個蹤跡的最后一個狀態(tài)不滿足于屬性。活力屬性的反例為一個指向循環(huán)的路徑，這個無限循環(huán)不包含應(yīng)有的狀態(tài)，它永遠無法到達特定的狀態(tài)。

3 有界模型檢驗的應(yīng)用

近年來，作為國內(nèi)外研究的熱點，BMC雖然發(fā)展迅速，但由于發(fā)展時間短，目前尚有很多不完善之處。對于BMC的不足之處，學(xué)術(shù)界主要從三個方面提高它的性能[5]。一、優(yōu)化BMC的轉(zhuǎn)換公式；二、在編碼時，優(yōu)化SAT實例變量的字句；三、將BMC問題轉(zhuǎn)化為SAT實例后，根據(jù)SAT子句的特點，優(yōu)化SAT工具，從而提高SAT求解效率。

BMC不僅廣泛應(yīng)用于系統(tǒng)安全、硬件設(shè)計、系統(tǒng)性能分析等領(lǐng)域，還被應(yīng)用于Web服務(wù)、實時調(diào)度和構(gòu)建技術(shù)等方面。其中，黃蔚等人將其用于C/C++程序內(nèi)存泄漏檢測方案[6]。駱翔宇等人利用有界模型檢驗對多智體系統(tǒng)的時態(tài)認(rèn)知的邏輯進行同步[7]。郝身剛等人使用有界模型檢驗對大規(guī)模服務(wù)進行建模，來解決傳統(tǒng)的服務(wù)組合技術(shù)靈活性差并且服務(wù)規(guī)模有限的問題[8]。

4 結(jié)束語

作為一種形式化的模型檢驗方法，BMC可以提高驗證的效率，同時也存在著很多問題。未來在軟件和硬件的形式化驗證領(lǐng)域，BMC仍然是一個熱點。

參考文獻：

[1] 侯剛， 周寬久， 勇嘉偉， 等. 模型檢測中狀態(tài)爆炸問題研究綜述[J]. 計算機科學(xué)， 2013， 40（6a）：77-86.

[2] 楊晉吉. 基于SAT的有界模型檢測及其應(yīng)用研究[D]. 廣州： 中山大學(xué)， 2008.

[3] 郭建， 韓俊剛. 基于不完全Kripke結(jié)構(gòu)三值邏輯的模型檢驗[J]. 計算機科學(xué)， 2006， 33（3）：263-266.

[4] Biere A， Cimatti A， Clarke E M， et al. Bounded Model Checking[C]// Advances in Computers. DBLP， 2003：117-148.

[5] 楊晉吉， 蘇開樂， 駱翔宇， 等. 有界模型檢測的優(yōu)化[J]. 軟件學(xué)報， 2009， 20（8）：2005-2014.

[6] 黃蔚， 洪玫， 楊秋輝， 等. 基于有界模型檢測的C/C++程序內(nèi)存泄露檢測[J]. 計算機應(yīng)用研究， 2016， 33（6）：1762-1766.

[7] 駱翔宇， 蘇開樂， 楊晉吉， 等. 有界模型檢測同步多智體系統(tǒng)的時態(tài)認(rèn)知邏輯[J]. 軟件學(xué)報， 2006， 17（12）：2485-2498.

[8] 郝身剛， 張麗. 有界模型檢測在服務(wù)組合中的應(yīng)用研究[J]. 計算機工程與應(yīng)用， 2012， 48（10）：111-114.