有界模型檢驗綜述

于露

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

關鍵詞：有界模型檢驗；模型檢驗；SAT

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

1 有界模型檢驗的概念

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

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

2 有界模型檢驗的過程

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

2.1 Kripke結構

有限狀態機可以被表示成kripke結構。

Kripke結構由狀態集、狀態之間的轉移關系、每個狀態上使一組原子命題為真的集合組成[3]。它的定義為：

定義一：設AP是一組原子命題，AP上的一個Kripke結構M定義為四元組M=（S，S0，R，L），其中：

1） S是一個有限狀態集合；

2） S0 ? S 是初始狀態集合；

3） R ? S×S 是轉移關系，要求是完全的，即對?s∈S都存在一個狀態?s‘∈S，使得（s，s）∈R成立；

4） L：S→2AP是一個函數，標記每個狀態使某些原子命題為真的函數。

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

Kripke結構是一種數學結構，目前在模型檢驗上是用比較多，可以表示為狀態圖。它可以用命題語句來表示狀態之間的轉移關系。使用Kripke結構來進行證明的優勢是：

1） 可以反映程序執行的狀態；

2） 程序的執行過程可以由狀態圖來表示。

2.2 線性時序邏輯

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

1） X（next）：下一個；

2） G（globally）：總是；

3） F（future）：未來；

4） U（until）：直到；

5） R（release）：釋放。

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

2.3 屬性的分類

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

3 有界模型檢驗的應用

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

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

4 結束語

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

參考文獻：

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

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

[3] 郭建， 韓俊剛. 基于不完全Kripke結構三值邏輯的模型檢驗[J]. 計算機科學， 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] 楊晉吉， 蘇開樂， 駱翔宇， 等. 有界模型檢測的優化[J]. 軟件學報， 2009， 20（8）：2005-2014.

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

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

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