模型檢測技術研究綜述

化希耀 蘇博妮 陳立平 高賢強*

(1 塔里木大學信息工程學院，新疆阿拉爾 843300)

(2 上海海事大學信息工程學院，上海 201306)

隨著計算機軟硬件系統集成度與復雜度的提高，系統的并發和高度交互等因素。給系統的行為帶來了不確定性，使得傳統的測試和仿真手段已無法確保系統的正確性和可靠性。形式化方法作為一種以嚴格數學理論為基礎的形式化描述方法，不僅可精確地描述系統的需求，而且可以對系統進行形式化驗證。形式化方法的這些特性使得它在軟硬件系統開發的各個階段得到了廣泛地應用。近年來該方法受到學術界和工業界的重視。

模型檢測是二十世紀最為成功的形式化驗證技術之一，它是由CMU的Clarke和Emerson、法國的Quielle 和 Sifakis 分別提出的［1，2］。1981 年，Clarke和他的博士生Emerson首次提出一個基于CTL的模型檢測算法，并開發了模型檢測工具SMV。模型檢測是通過對有限狀態系統的窮舉搜索來實現驗證的技術，其面臨的主要困難是狀態空間爆炸問題。1987年，CMU的博士生McMillan［3］采用有序二叉決策圖(OBDDs)［4］隱式地表示系統的遷移關系。他們將這種方法命名為符號模型檢測，并在SMV的基礎上開發了一個新的模型檢測工具NuSMV。符號模型檢測可以檢測的系統狀態數達10120以上，這極大地推動了模型檢測技術的應用。在隨后的若干年里，研究者們紛紛提出各種狀態約簡算法，并開發了許多經典的模型檢測工具。

1 模型檢測基本原理和過程

1.1 模型檢測基本原理

模型檢測的基本原理［5］是用狀態遷移系統(S)表示待檢測系統的邏輯行為，用時態邏輯公式(φ)描述系統所期望的性質。這樣該問題就轉化為S滿足公式φ。從直觀上說，S為待檢測系統的抽象模型，常用的描述方法如有窮狀態自動機和進程代數等，而屬性公式φ則常用時態邏輯描述，如線性時態邏輯LTL。模型檢測是對系統模型的狀態空間進行完全搜索的:檢測系統的每一個狀態是否滿足期望的性質。

1.2 模型檢測的過程

1.2.1 系統建模(Modeling)

對系統建模首先選用一種形式化描述方法，將待驗證的系統設計轉化為工具所能接受的模型，比如狀態遷移圖。通常建模中會采用抽象的方法去除不重要或不相關的細節，以避免引入過多的細節而引起狀態爆炸。

1.2.2 性質描述(Specification)

系統所要驗證的性質通常是采用邏輯公式來描述，比如時態邏輯。它能夠描述系統隨著時間變化而引起的行為變化。模型檢測提供了許多驗證模型是否滿足性質的方法，但這并不能保證這些性質包含所有系統所要滿足的性質。因此這就要求設計人員在性質描述時要保證性質的完整性。

1.2.3 系統驗證(Verification)

系統驗證是通過模型檢測算法對系統的狀態空間進行窮盡搜索。驗證結束后，如果未發現違反性質描述的狀態，則表明該模型滿足期望的性質;否則給出一個反例路徑，供設計人員參考。錯誤發生的原因可能是由于不正確的系統建模或是錯誤的性質描述，設計人員可根據反例路徑分析其原因，修改后重新驗證。模型檢測的過程如圖1所示。

圖1 模型檢測的過程

2 狀態爆炸問題

在起初的模型檢測算法實現時，系統的狀態和狀態間的遷移都是采用顯式的狀態遷移圖來表示。這種方法對那些進程數量較少的并發系統非常實用。而當并發進程分量較多時，系統的全局狀態空間會隨著并發量的增加，呈指數增長，即產生狀態爆炸問題［5］。狀態爆炸問題是阻礙模型檢測技術應用的瓶頸。目前，研究人員已經提出許多緩解狀態爆炸問題的有效方法，包括符號模型檢測、On－thefly技術、偏序歸約和抽象技術等。

2.1 符號模型檢測

符號模型檢測［3］是采用布爾公式來隱式表示系統的狀態和遷移的方法。該方法基于Bryant［4］提出的有序二叉決策圖OBDD。由于OBDD提供了比合取范式和析取范式更為壓縮的布爾公式的范式，以及許多有效的操作算法，所以符號模型檢測可用來驗證狀態數更多的系統。目前該方法可驗證的狀態數超過了10120。

2.2 On－the－fly技術

On － the－ fly［5］技術也稱為局部模型檢測，是指驗證之前不必展開系統所蘊含的所有狀態，而是按待驗證模型性質的需要，只產生部分和必要的系統狀態。該方法目前被絕大部分模型檢測工具所采用。

2.3 偏序歸約

在一個系統的并發執行的事件中，如果兩個事件以任意的次序執行得到相同的全局狀態，則稱這兩個事件是獨立的。通常一個系統是由多個進程并發執行，而大部分的用來描述并發系統性質的邏輯無法區分交替序列中按不同次序執行的兩個獨立事件，所以通常要考慮所有可能的交替序列，從而導致狀態爆炸問題。偏序歸約［5］的基本思想就是減少驗證本質上相同的事件交替序列，只考慮其中一種執行路徑。

2.4 抽象技術

抽象［6］是指去除系統中不必要的細節而產生較小的系統模型。常見的抽象技術包括狀態合并、數據抽象和謂詞抽象。狀態合并是通過去除不影響系統規范中變量狀態，得到一個簡化的自動機模型。數據抽象是一種通用性很強的抽象技術，其基本思想是通過去掉系統的部分信息來構造狀態數較小的系統模型。當系統變量的定義域為無窮域時，將導致系統擁有無窮狀態，而通常所需驗證的系統性質與系統變量的具體值無關，因此可以在系統的精確數據值和一個小的抽象數據值之間建立一個映射關系，通過這種映射關系可以構造一個比實際系統較小的抽象系統。謂詞抽象實現了自動將無窮狀態系統映射到有窮狀態系統的方法，該技術被廣泛應用在對軟件系統抽象中。

3 模型檢測工具

模型檢測的優點是可以完全自動地進行驗證，這主要歸功于許多成熟的模型檢測工具的支持。開發新的模型檢測工具也是模型檢測技術研究的主要內容。目前國際上有許多成熟的模型檢測工具，包括:

3.1 SPIN

SPIN［7］(Simple Promela Interpreter)是一款運行在Linux/Unix環境下的開源軟件驗證工具，由美國貝爾實驗室于1980年開發，可用來對多線程軟件應用進行驗證。SPIN使用PROMELA語言和LTL對系統和其性質進行描述，并集成了on－the－fly、偏序歸約和多核/并行等多種模型檢測技術。目前該工具被廣泛地應用在操作系統、數據通信協議、并發算法、鐵路信號協議、航天器控制軟件和核電站等領域邏輯設計驗證中。SPIN于2002年4月榮獲ACM軟件系統獎。

3.2 NuSMV

NuSMV［8］是由CMU和FBK－IRST聯合研制的對有限狀態系統進行形式化驗證的工具。NuSMV是在SMV的基礎上開發的，并對其進行了擴充和升級。其同時支持批處理、命令行式和圖形界面三種交互方式。NuSMV采用SMV形式語言描述系統，通過符號模型檢測和有界模型檢測等技術來分析以CTL和 LTL表達系統的性質。1992年 CMU的Clarke和他的學生使用SMV對IEEE Futurebus+緩存一致性協議進行驗證，發現了一些協議設計中潛在的錯誤。

3.3 UPPAAL

UPPAAL［9］是由瑞士的 Uppsala大學和丹麥的Aalborg大學聯合開發的模型檢測工具。它主要采用時間自動機網絡對實時系統進行建模、確認和驗證。UPPAAL適用于對具有有限控制結構和實數值時鐘的不確定性進程集、通過信道和共享變量通信的系統進行驗證。其典型的應用領域包括實時控制器和通信協議尤其是那些對時間方面要求較高的協議。

3.4 PAT

PAT［10］(Process Analysis Toolkit)是由新加坡國立大學PAT小組開發的對并發和實時系統進行建模、仿真和驗證的模型檢測工具。PAT采用CSP#語言對系統建模、LTL描述系統性質，集成了偏序歸約、對稱歸約和并行模型檢測等多種優化技術。另外PAT以其友好的用戶界面和開放的框架受到諸多用戶的青睞，目前該工具已被來自62個國家和地區的2500+個用戶使用。

傳統的模型檢測工具都只面向一個特定的領域，如 UPPAAL支持實時系統的驗證、SPIN和NuSMV都只支持常規并發系統的模型檢測，而PAT集成了多種建模語言，面向的領域包括并發、實時和概率等系統的模型檢測。據PAT小組的最新論文表明，用戶使用PAT可以在1至2個月內開發出面向具體應用領域的模型檢測工具。表1［11］是對上述工具的對比。

表1 模型檢測工具比較

4 模型檢測技術的重要研究領域

模型檢測技術自從誕生之日起，已經歷了三十余年的發展，在學術界和工業界都引起了廣泛的關注。在工業界包括Microsoft、Intel、Google和IBM 等巨頭公司先后斥巨資研究該技術并成功地將其應用到實際的產品開發中，取得了巨大的經濟效益。在學術界許多世界一流的高校和研究所將模型檢測作為理論計算機科學研究的重點方向之一，如美國卡內基梅隆大學和貝爾實驗室、英國牛津大學和伯明翰大學、國內的中科院軟件研究所、南京大學、同濟大學和吉林大學等。

目前，國內外對模型檢測技術的研究熱點主要集中在以下幾個方面。

4.1 將模型檢測技術應用到新的領域:模型檢測技術在計算機硬件、安全認證協議等方面的驗證已經非常成熟，近年來隨著計算機運算速度的大幅提升和大容量存儲器的出現，以及各種新的緩解狀態爆炸問題的算法的提出，為將模型檢測技術應用到新的領域奠定了基礎。①軟件模型檢測［12］是指對軟件的需求分析或源代碼進行形式化驗證的技術。由于軟件中存在復雜的數據結構、取值空間無限的數據類型等原因，使得狀態爆炸問題顯得尤為突出。近年來隨著抽象技術的應用，大大緩解了上述問題，并出現了許多軟件模型檢測工具，如SLAM、JPF和BLAST 等。②實時系統與混成系統［13，14］是工業控制和軍事領域應用比較廣泛的系統。前者是指在限定的時間內系統對外界的輸入產生響應的系統，后者是指既包括連續動態子系統，也包括離散動態子系統的系統。如何保證這兩種系統的可靠性是計算機科學和控制理論研究的重要課題。通常采用時間自動機、時間CSP、混成自動機和混成Petri網等形式化方法描述系統模型，著名的工具如UPPAAL等。④智能規劃是人工智能領域研究的熱點問題。規劃問題是指在問題域中給定一個初始狀態、一個目標狀態和一些行為，找到一個從初始狀態到目標狀態的行為序列。將模型檢測搜索算法應用到規劃問題求解中，是當前模型檢測技術的應用新方向，并且已開發出一些基于模型檢測技術的規劃器，如MIPS［15］系統。⑤軟件體系結構在系統設計描述中扮演著重要的角色，但缺乏形式化描述和驗證方法的支持阻礙了軟件體系結構建模的發展。目前已提出了幾種體系結構描述語言，如 Wright［16］和 Darwin［17］等。

4.2 模型檢測算法的研究:為解決狀態爆炸問題，研究者們先后提出了許多有效的方法。除了本文第三節闡述的四種方法以外，還有對稱技術、組合推理和有界模型檢測等。①對稱技術［13，14］的基本思想是:多并發進程系統執行時可能會產生許多相同或相似路徑，可以只搜索對稱關系中等價的一種情形，以避免重復搜索對稱或相同的系統狀態。對稱技術通過劃分等價類來達到約簡狀態空間的目的，它只考慮等價類中的一種情形，以此類推同類的其它情形。②組合推理［13，14］采用分而治之的辦法，將待驗證的系統分解為小的模塊，分別對這些小模塊進行性質驗證，再由這些小模塊的性質組合推斷整個系統的性質。③有界模型檢測［5］是基于SAT技術的符號模型檢測技術，其基本思想是根據狀態轉換關系將系統狀態轉換展開K次，得到所有長度為K的狀態轉換路徑，然后在其中搜索一個反例。如果沒有找到反例，則驗證過程將K不斷加1，直到找到一個反例或到達預先設好的上界，則搜索終止。

4.3 模型檢測工具的研制:模型檢測技術的應用要靠工具的支持，同時各類工具的應用也使得模型檢測技術得到了極大的推廣。除了在上文第四節介紹的模型檢測工具SPIN、NuSMV、UPPAAL和 PAT之外，還有SLAM、JPF(Java Path Finder)和BLAST等。①SLAM［18］是Microsoft公司開發的一款軟件模型檢測工具。該工具可以對C程序進行靜態地分析以確定它是否違反給定API的使用規則。SLAM已被成功地應用到Windows XP驅動程序的有效性驗證中，并發現了一些調用內核API的錯誤。②JPF［19］是由NASA開發的JAVA程序驗證工具。它集成了模型檢測、程序分析和測試功能，采用的狀態約簡技術有偏序歸約、切片技術、抽象和運行時分析技術等。NASA使用JPF驗證一個實時航空電子設備操作系統并發現了一個潛在的錯誤。④BLAST［20］是加州大學伯克利分校開發的C程序驗證工具。該工具在反例引導謂詞抽象求精技術上，提出了懶惰謂詞抽象技術，大大提高了可驗證程序的規模。

4.4 模型檢測技術與其它技術相結合:將模型檢測技術與其它驗證技術結合起來，發揮各自的優勢是當前該領域的研究熱點之一。①與概率論方法(如馬爾科夫鏈)相結合稱為概率模型檢測［13，14］，該方法不僅可以檢測出系統是否可能有錯，而且還可以給出發生錯誤的概率。常見的概率模型有離散時間馬爾科夫鏈、概率自動機等，比較出名的概率模型檢測工具如PRISM。②與定理證明相結合是目前最有前景的一種方法［13，14］，其基本思想是將模型檢測作為演繹框架內的一個決策過程，也可以先使用演繹推理獲取系統的一個有限狀態抽象系統，然后對該抽象系統進行模型檢測。

5 小結

目前，模型檢測技術已被廣泛地應用在計算機硬件設計、通信協議、控制系統和安全認證協議等領域，取得了巨大的成功。例如Microsoft和Intel等許多公司均已采用該技術驗證產品的正確性。為表彰Clarke、Emerson和Quielle、Sifakis等人在模型檢測領域所做出的突出貢獻，2007年美國計算機協會(ACM)授予他們ACM圖靈獎。

保障日益復雜的軟硬件系統的可靠性和安全性，是研究者們正在努力研究的難題。建立在嚴格數學理論基礎之上的形式化方法必將在這之中占據主導地位，且已從實驗室成功走向工業應用，并產生了許多豐碩的成果。本文從模型檢測技術的背景入手，詳細闡述了該技術的基本原理和發展現狀，并對幾款成熟的模型檢測工具做了對比分析，總結了近年來模型檢測技術在國內外的研究進展，為今后進一步研究相關技術提供參考和借鑒。

模型檢測是一個發展非常快的研究方向，在最近的一些研究論文中有人將其應用到了生物系統和智能電網的分析和驗證中，取得了新穎的效果。深入研究模型檢測技術將為今后可信軟件、更高效硬件系統及其它復雜系統的設計研究提供更佳的手段與方法。

［1］Clarke E M，Emerson E A，Sistla A P.Automatic verification of finite－state concurrent systems using temporal logic specifications［J］.ACM Transactions on Programming Languages and Systems(TOPLAS)，1986，8(2):244－263.

［2］Clarke Edmund M.The Birth of Model Checking［A］.Symposium 25 Years of Model Checking［C］.Berlin:Springer Heidelberg，2008:1 －26.

［3］Burch J R，Clarke E M，McMillan K L，et al.Symbolic model checking:1020 states and beyond［J］.Information and computation，1992，98(2):142－170.

［4］Bryant R E.Graph－based algorithms for Boolean function manipulation［J］.IEEE Transactions on Computers，1986，100(8):677－691.

［5］Clarke E M，Grumberg O，Peled D.Model Checking［M］.Cambridge:The MIT Press，1999:1 －201.

［6］Clarke E M，Grumberg O，Long D E.Model checking and abstraction［J］.ACM Transactions on Programming Languages and Systems(TOPLAS)，1994，16(5):1512－1542.

［7］Holzmann G J.The model checker SPIN［J］.IEEE Transactions on Software Engineering，1997，23(5):279－295.

［8］Cimatti A，Clarke E，Giunchiglia F，et al.NuSMV:a new symbolic model checker［J］.International Journal on Software Tools for Technology Transfer，2000，2(4):410－425.

［9］Bengtsson J，Larsen K，Larsson F，et al.UPPAAL—a tool suite for automatic verification of real－time systems［M］.Springer Berlin Heidelberg，1996:1－204.

［10］Sun J，Liu Y，Dong J S，et al.PAT:Towards flexible verification under fairness［A］.Computer Aided Verification Springer Berlin Heidelberg，2009:709－714.

［11］Liu Y，Sun J，Dong J S.Developing modle chedkers using PAT［M］Automated Tehnology for verificatom and Analysis.Sringer Berdin Heidelberg，2010:371 －377.

［12］Visser W，Havelund K，Brat G，et al.Model checking programs［A］.The Fifteenth IEEE International Conference on Automated Software Engineering［C］.IEEE，2000:3－11.

［13］林惠民，張文輝.模型檢測:理論、方法與應用［J］.電子學報，2002(S1):1907－1921.

［14］戎玫，張廣泉.模型檢測新技術研究［J］.計算機科學，2003(5):102－104.

［15］Edelkamp S，Helmert M.MIPS:The model－checking integrated planning system［J］.AI magazine 22.3(2001):67.

［16］Allen R，Garlan D.A formal basis for architectural connection［J］.ACM Transactions on Software Engineering and Methodology(TOSEM)，1997，6(3):213－249.

［17］Magee J，Kramer J.Dynamic structure in software architectures［A］.ACM SIGSOFT Software Engineering Notes［C］.ACM，1996，21(6):3－14.

［18］Ball T，Rajamani S K.The SLAM toolkit［A］.Computer aided verification［C］.Springer Berlin Heidelberg，2001:260－264.

［19］Havelund K.Java PathFinder，a translator from Java to Promela［J］.Lecture notes in computer science，1999:152－152.

［20］Beyer D，Henzinger T A，Jhala R，et al.The software model checker Blast［J］.International Journal on Software Tools for Technology Transfer，2007，9(5 － 6):505－525.