有界模型檢驗(yàn)綜述

于露

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

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

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

1 有界模型檢驗(yàn)的概念

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

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

2 有界模型檢驗(yàn)的過程

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

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

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

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

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

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

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

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

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

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

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

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

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

2.2 線性時(shí)序邏輯

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

1） X（next）：下一個(gè)；

2） G（globally）：總是；

3） F（future）：未來；

4） U（until）：直到；

5） R（release）：釋放。

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

2.3 屬性的分類

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

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

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

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

4 結(jié)束語

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

參考文獻(xiàn)：

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

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

[3] 郭建， 韓俊剛. 基于不完全Kripke結(jié)構(gòu)三值邏輯的模型檢驗(yàn)[J]. 計(jì)算機(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é)報(bào)， 2009， 20（8）：2005-2014.

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

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

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