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

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

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

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

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

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

1.1 模型檢測基本原理

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

1.2 模型檢測的過程

1.2.1 系統(tǒng)建模(Modeling)

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

1.2.2 性質(zhì)描述(Specification)

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

1.2.3 系統(tǒng)驗證(Verification)

系統(tǒng)驗證是通過模型檢測算法對系統(tǒng)的狀態(tài)空間進行窮盡搜索。驗證結(jié)束后，如果未發(fā)現(xiàn)違反性質(zhì)描述的狀態(tài)，則表明該模型滿足期望的性質(zhì);否則給出一個反例路徑，供設(shè)計人員參考。錯誤發(fā)生的原因可能是由于不正確的系統(tǒng)建?；蚴清e誤的性質(zhì)描述，設(shè)計人員可根據(jù)反例路徑分析其原因，修改后重新驗證。模型檢測的過程如圖1所示。

圖1 模型檢測的過程

2 狀態(tài)爆炸問題

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

2.1 符號模型檢測

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

2.2 On－the－fly技術(shù)

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

2.3 偏序歸約

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

2.4 抽象技術(shù)

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

3 模型檢測工具

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

3.1 SPIN

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

3.2 NuSMV

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

3.3 UPPAAL

UPPAAL［9］是由瑞士的 Uppsala大學和丹麥的Aalborg大學聯(lián)合開發(fā)的模型檢測工具。它主要采用時間自動機網(wǎng)絡(luò)對實時系統(tǒng)進行建模、確認和驗證。UPPAAL適用于對具有有限控制結(jié)構(gòu)和實數(shù)值時鐘的不確定性進程集、通過信道和共享變量通信的系統(tǒng)進行驗證。其典型的應(yīng)用領(lǐng)域包括實時控制器和通信協(xié)議尤其是那些對時間方面要求較高的協(xié)議。

3.4 PAT

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

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

表1 模型檢測工具比較

4 模型檢測技術(shù)的重要研究領(lǐng)域

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

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

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

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

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

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

5 小結(jié)

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

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

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

［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］林惠民，張文輝.模型檢測:理論、方法與應(yīng)用［J］.電子學報，2002(S1):1907－1921.

［14］戎玫，張廣泉.模型檢測新技術(shù)研究［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.