模型檢測(cè)技術(shù)研究綜述

化希耀 蘇博妮 陳立平 高賢強(qiáng)*

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

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

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

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

1 模型檢測(cè)基本原理和過程

1.1 模型檢測(cè)基本原理

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

1.2 模型檢測(cè)的過程

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

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

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

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

1.2.3 系統(tǒng)驗(yàn)證(Verification)

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

圖1 模型檢測(cè)的過程

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

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

2.1 符號(hào)模型檢測(cè)

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

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

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

2.3 偏序歸約

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

2.4 抽象技術(shù)

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

3 模型檢測(cè)工具

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

3.1 SPIN

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

3.2 NuSMV

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

3.3 UPPAAL

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

3.4 PAT

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

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

表1 模型檢測(cè)工具比較

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

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

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

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

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

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

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

5 小結(jié)

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

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

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

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

［14］戎玫，張廣泉.模型檢測(cè)新技術(shù)研究［J］.計(jì)算機(jī)科學(xué)，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.