模型檢驗(yàn)(閔應(yīng)驊)

1、.模型檢驗(yàn)（ 1）（ 091230 ）大家承認(rèn)，計(jì)算機(jī)領(lǐng)域的ACM 圖靈獎(jiǎng)相當(dāng)于自然科學(xué)的諾貝爾獎(jiǎng)。2007 年圖靈獎(jiǎng)授予Edmund M. Clarke，E. Allen Emerson,和 Joseph Sifakis。他們創(chuàng)立了模型檢驗(yàn)- 一種驗(yàn)證技術(shù)，用算法的方式確定一個(gè)硬件或軟件設(shè)計(jì)是否滿足用時(shí)態(tài)邏輯表述的形式規(guī)范。如果不能滿足， 則提供反例。他們?cè)?981 年提出這個(gè)方法，經(jīng)過28 年的發(fā)展，已經(jīng)在VLSI 電路、通信協(xié)議、軟件設(shè)備驅(qū)動(dòng)器、 實(shí)時(shí)嵌入式系統(tǒng)和安全算法的驗(yàn)證方面得到了實(shí)際應(yīng)用。相應(yīng)的商業(yè)工具也已出現(xiàn)，估計(jì)今后將對(duì)未來(lái)的硬件和軟件產(chǎn)業(yè)產(chǎn)生重大影響。2009 年 11 月

2、 CACM 發(fā)表了三位對(duì)模型檢驗(yàn)的新的詮釋。本人將用幾次對(duì)他們的詮釋做一個(gè)通俗的介紹，對(duì)我自己也是一個(gè)學(xué)習(xí)的過程。Edmund M. Clarke現(xiàn)在是美國(guó)卡內(nèi)基梅隆大學(xué)（ CMU ）計(jì)算機(jī)科學(xué)系教授。E. Allen Emerson是在美國(guó)奧斯汀的德州大學(xué)計(jì)算機(jī)科學(xué)系教授。Joseph Sifakis是法國(guó)國(guó)家科學(xué)研究中心研究員，Verimag 實(shí)驗(yàn)室的創(chuàng)立者。模型檢驗(yàn)（ 2）（ 091231 ）程序正確性的形式驗(yàn)證依靠數(shù)學(xué)邏輯的使用。程序是一個(gè)很好定義了的、可能很復(fù)雜、直觀上不好理解的行為。而數(shù)學(xué)邏輯能精確地描述這些行為。過去，人們傾向于正確性的形式證明。而模型檢驗(yàn)回避了這種證明。在上世紀(jì)

3、60 年代，流行的是佛洛伊德-霍爾式的演繹驗(yàn)證。這種辦法像手動(dòng)證明一樣，使用公理和推論規(guī)則，比較困難，而且要求人的獨(dú)創(chuàng)性。一個(gè)很短的程序也許需要很長(zhǎng)的一個(gè)證明。不搞程序正確性證明，可以使用時(shí)態(tài)邏輯，一種按時(shí)間描述邏輯值變化的形式化。如果一個(gè)程序可以用時(shí)態(tài)邏輯來(lái)指定，那它就可以用有限自動(dòng)機(jī)來(lái)實(shí)現(xiàn)。模型檢驗(yàn)就是去檢驗(yàn)一個(gè)有限狀態(tài)圖是否是一個(gè)時(shí)態(tài)邏輯規(guī)范的一個(gè)模型。對(duì)于正在運(yùn)行的并發(fā)程序，它們一般是非確定性的，像硬件電路、微處理器、操作系統(tǒng)、銀行網(wǎng)絡(luò)、通信協(xié)議、汽車電子及近代醫(yī)學(xué)設(shè)備。時(shí)態(tài)邏輯所用的基本算子是F（有時(shí)）， G（總是），X（下一次），U （直到）?，F(xiàn)在叫線性時(shí)間邏輯（LTL ）。.另一

4、種常用的邏輯是計(jì)算樹邏輯（CTL ）。它的基本時(shí)態(tài)是A （對(duì)所有以后的交易），E （對(duì)某些以后的交易），跟隨著F， G， X， U 之一。復(fù)合公式是線性時(shí)間邏輯子公式的嵌套和組合。例如 AFp （以后， p 終將成立，因此是必然的。）EFp （以后， p 最后可能成立。）如圖 1所示。時(shí)態(tài)邏輯公式可以在給定的有限狀態(tài)圖上加以解釋。所以又稱為克里普克（kripke ）結(jié)構(gòu)。 M包含一個(gè)狀態(tài)集 S ，一個(gè)完全的二進(jìn)制轉(zhuǎn)換關(guān)系R ? S S, 和一個(gè)狀態(tài)標(biāo)簽L ，其原子事實(shí)為真。用 M, s0 |= f表示 “在結(jié)構(gòu) M 中，于狀態(tài)s0， f 為真。 ”或者簡(jiǎn)寫為 M |= f. 例如， M, s0

5、 |= AFp當(dāng)且僅當(dāng)對(duì)在 M中的所有通路x = s0, s1, s2, . . . 我們有對(duì)任何 i =0, P L(si).當(dāng)我們寫規(guī)范的時(shí)候，我們只寫AFp ，斷言公式 p 是必然的。一個(gè)線性時(shí)間邏輯公式h 意味著在整個(gè)結(jié)構(gòu)皆為真，即 Ah 。在線性時(shí)間邏輯中，G? (C1 C2) 表明進(jìn)程 C1和 C2總是互相排斥的。而在計(jì)算樹邏輯中則寫成 AG? (C1 C2) 。AG(T1 ?AFC1) 意味著只要進(jìn)程1 進(jìn)入它的嘗試區(qū)域 T1 ，它總是進(jìn)入它的關(guān)鍵段 C1 。AGEFstart表示系統(tǒng)總是可以重新啟動(dòng)的。這在線性時(shí)間邏輯中是無(wú)法表示的。而 CTL* 中的 EGFsend 則表明存

6、在一個(gè)公平的行為，使得send 條件可以重復(fù)出現(xiàn)。這些邏輯已經(jīng)在工業(yè)界得到廣泛應(yīng)用，包括基于CTL 的 IBM Sugar ，基于 LTL 的 IntelFor-Spec ，和 IEEE 1850標(biāo)準(zhǔn)所用的 PSL 用了 CTL* 。還有命題演算，非常一般的TL。它允許時(shí)態(tài)正確性的不動(dòng)點(diǎn)遞歸定義。例如EFp = pEX(EFp) 。時(shí)態(tài)正確性的不動(dòng)點(diǎn)特征在模型檢驗(yàn)的算法和工具中都很有用。模型檢驗(yàn)（ 3）（ 091231 ）時(shí)態(tài)邏輯用來(lái)描述正確的系統(tǒng)行為，模型檢驗(yàn)提供實(shí)用的硬件和軟件驗(yàn)證方法。模型驗(yàn)證可形式地描述如下：給定一個(gè)有限結(jié)構(gòu)M，狀態(tài) s，和一個(gè)時(shí)態(tài)邏輯公式，問M, s |= f ? 即

7、問：在結(jié)構(gòu)M 中，于狀態(tài)s0 ，f 是否為真？或者說(shuō)，給定M 和 f,計(jì)算這個(gè)集合s : M, s |= f 。他們證明了這個(gè)問題的計(jì)算復(fù)雜性對(duì)公式和結(jié)構(gòu)的大小是線性的。該算法是基于基本時(shí)態(tài)模型化的不動(dòng)點(diǎn)原理。例.如，如果 f(Z) 表示 p AXZ 。 AFp = f (AFp) 是 f(Z) 的不動(dòng)點(diǎn)。因?yàn)?AFp 為真，當(dāng)且僅當(dāng)p 為真，或者 AXAFp 為真。（意即以后 p 總會(huì)為真，當(dāng)且僅當(dāng)p 現(xiàn)在就真，或者以后總會(huì)為真。）一般來(lái)說(shuō)，可能有許多不動(dòng)點(diǎn)，但這個(gè)是最小不動(dòng)點(diǎn)，記為Z = f (Z) 。我們可以迭代地計(jì)算使得AFp 為真的狀態(tài)集。因?yàn)槊恳粋€(gè)公式都有一個(gè)使之為真的狀態(tài)集?？梢?/p>

8、證明，單調(diào)遞增序列 false? f ( false)?f 2(false)?. . .?f k( false) = f k+1(false)揭示最小不動(dòng)點(diǎn)，如果f(Z) 是單調(diào)的。 CTL 模型驗(yàn)證是多項(xiàng)式復(fù)雜的，但LTL 則是指數(shù)復(fù)雜的，不過可以接受。問題是時(shí)態(tài)邏輯公式的可表達(dá)性。就是說(shuō)， 什么樣的特性可以用時(shí)態(tài)邏輯公式來(lái)表達(dá)？例如安全性（ “無(wú)壞事發(fā)生 ”即 G-bad ），活性（ “有些好事發(fā)生 ”，即 Fgoal ），及公平性（ “有些事常發(fā)生 ” 即 GFtry ）。我們需要用表達(dá)式表達(dá)所有正確性。如果這一點(diǎn)做不到，就無(wú)法使用模型檢驗(yàn)。但實(shí)際上，時(shí)態(tài)邏輯公式能夠做到這一點(diǎn)，而且接近

9、自然語(yǔ)言。正因?yàn)檫@一點(diǎn)，我們需要LTL ， CTL ，和 CTL* 。另一個(gè)問題是簡(jiǎn)潔性，即表達(dá)是否簡(jiǎn)潔。例如CTL* 公式 E(Fp1 Fp2) 不是一個(gè)CTL 公式，但它等價(jià)于EF(p1 EFp2) EF(p2 EFp1), 這是一個(gè)CTL 公式，雖然它比較長(zhǎng)一些。另一個(gè)重要問題是有效性，即對(duì)于電路或邏輯， 模型驗(yàn)證問題的復(fù)雜性及模型驗(yàn)證算法的性能。當(dāng)然，可表達(dá)性、簡(jiǎn)潔性和有效性是有矛盾的，需要某些折中。一般要求M 少于 1,000,000個(gè)狀態(tài)。對(duì)于狀態(tài)特別多的機(jī)器，可以設(shè)法省略一些非本質(zhì)的詳情，以簡(jiǎn)化M。有人也提出用所謂符號(hào)模型檢驗(yàn)來(lái)處理復(fù)雜的機(jī)器。這方面的研究還很多，有人甚至考慮無(wú)限

10、狀態(tài)系統(tǒng)。模型檢驗(yàn)（ 4）（ 091231 ）模型檢驗(yàn)的成功之處在于它用自動(dòng)搜索代替手動(dòng)證明來(lái)解決驗(yàn)證的問題。模型檢驗(yàn)包括三部分： 1 ?；诿}時(shí)態(tài)邏輯的規(guī)范語(yǔ)言，2 。表示被驗(yàn)證系統(tǒng)的編碼狀態(tài)機(jī)的方法，3。驗(yàn)證算法，對(duì)狀態(tài)空間的智能搜索以確定規(guī)范是真還是假。如果規(guī)范沒有被實(shí)現(xiàn)，模型檢驗(yàn)?zāi)軌蚪o出反例。這一條非常重要，因?yàn)樗鼛椭覀僤ebug 。如圖 2 所示。狀態(tài)爆炸是模型檢驗(yàn)中的一個(gè)大問題，因?yàn)楝F(xiàn)在的復(fù)雜系統(tǒng)，其狀態(tài)數(shù)都是天文數(shù)字。n 個(gè)相互異步的進(jìn)程，如果每個(gè)進(jìn)程有m 個(gè)狀態(tài)，其狀態(tài)數(shù)為m 的 n 次方（ mn) 。近年來(lái)，正是在這方面有許多突破。有序的二進(jìn)制判決圖（OBDD ）提供了處

11、理大系統(tǒng)進(jìn)行符號(hào)模型檢驗(yàn)的可能性。例如某些具有1020 狀態(tài)的實(shí)例進(jìn)行了符號(hào)模型檢驗(yàn)。軟件進(jìn)程之間往往是異步的，狀態(tài)數(shù)就會(huì)指數(shù)級(jí)增加。兩個(gè)事件稱為是獨(dú)立的，如果不論它們按什么順序執(zhí)行，其結(jié)果是相同的整體狀態(tài)。用偏序簡(jiǎn)化方法可以部分地解決異步進(jìn)程的狀態(tài)爆炸問題。近年來(lái)，布爾可滿足性問題（SAT ）的進(jìn)展，對(duì)模型檢驗(yàn)提出了有界模型檢驗(yàn)（BMC ）對(duì)硬件設(shè)計(jì)驗(yàn)證特別有效。 其主要想法如下。 假如要檢驗(yàn)形如 Fp 的性質(zhì)， BMC 要確定是否存在一個(gè)長(zhǎng)度為 k 的反例， 即是否存在一條長(zhǎng)度為 k 的通路， 結(jié)束于一個(gè)循環(huán)， 其每一個(gè)狀態(tài)都有 ?p 。這里所謂有界就是指這個(gè) k。有人對(duì) 9510 個(gè)鎖存

12、器和 9499 個(gè)輸入的電路做了 BMC 。.抽象映射是簡(jiǎn)化模型檢驗(yàn)的另一種方法，如圖 4 所示， 把一堆狀態(tài)簡(jiǎn)化為一個(gè)狀態(tài)。原來(lái)系統(tǒng)稱為具體系統(tǒng)， 而簡(jiǎn)化了的系統(tǒng)稱為抽象系統(tǒng)。抽象系統(tǒng)能夠保持具體系統(tǒng)的許多性質(zhì)，但也會(huì)丟失某些性質(zhì)。已有許多結(jié)果揭示這一問題。狀態(tài)爆炸的問題已經(jīng)有了許多的研究，但是，并沒有完全解決。這正是未來(lái)要解決的問題。模型檢驗(yàn)（ 5）（ 100101 ）模型檢驗(yàn) (model checking)自從 1981 年提出來(lái)以后，受到各種非議。至今28 年過去了，才得到了學(xué)術(shù)界和工業(yè)界的廣泛關(guān)注。這是很正常的。要求一個(gè)學(xué)術(shù)成果馬上用于實(shí)際，很不現(xiàn)實(shí)。中.國(guó)某些干部就這么急功近利。

13、算法的設(shè)計(jì)驗(yàn)證包括三步：（ 1 ）需求規(guī)范； （ 2）建立可執(zhí)行的系統(tǒng)模型；（ 3 ）開發(fā)可擴(kuò)展的算法，一是去檢驗(yàn)需求，二是當(dāng)需求不能滿足時(shí)進(jìn)行診斷。需求規(guī)范可以用兩種方式給定。一種是基于狀態(tài)的需求，用轉(zhuǎn)換系統(tǒng)指明系統(tǒng)的可觀察行為；另一種是基于特性的需求，用說(shuō)明性的方式。 這些需求用一系列的時(shí)態(tài)邏輯公式表達(dá)。IEEE 的 PSL語(yǔ)言就用了這二者的組合。需求規(guī)范的無(wú)矛盾性和完全性仍然是一個(gè)問題。現(xiàn)在還缺乏某些外部需求的形式化，例如安全性（隱私），可重構(gòu)性（不相互干擾的構(gòu)造性），服務(wù)質(zhì)量（抖動(dòng)度）等?？蓤?zhí)行的模型要求忠實(shí)性，即模型必須與被驗(yàn)證系統(tǒng)保持語(yǔ)義，而且必須是可檢驗(yàn)的。這樣，你驗(yàn)證的特性才能

14、在實(shí)際系統(tǒng)中實(shí)現(xiàn)。為了避錯(cuò)和糾錯(cuò)，模型應(yīng)該能從系統(tǒng)描述自動(dòng)產(chǎn)生。對(duì)于硬件驗(yàn)證，此事從RTL 描述出發(fā)，比較容易完成。而對(duì)于軟件，可能只能在抽象級(jí)別上進(jìn)行。擴(kuò)展UML 進(jìn)行調(diào)度和資源管理無(wú)法提供嚴(yán)格的定時(shí)特性。而擴(kuò)展硬件描述語(yǔ)言，像SystemC 和 TLM由于缺乏形式語(yǔ)義只能用于模擬?？蓴U(kuò)展的驗(yàn)證方法對(duì)大系統(tǒng)不好做。一個(gè)解決辦法是根據(jù)特定的語(yǔ)義范疇開發(fā)抽象技術(shù)，即在特定語(yǔ)義領(lǐng)域求解不動(dòng)點(diǎn)方程。另一個(gè)解決辦法是面對(duì)復(fù)雜性，用分而治之的途徑。過去，特性被分成兩部分：階段-結(jié)論?，F(xiàn)在，我們需要組合驗(yàn)證的理論，把驗(yàn)證組合起來(lái)，形成一個(gè)大的驗(yàn)證。計(jì)算機(jī)工程于其他自然科學(xué)一個(gè)巨大的不同就在于保證正確的驗(yàn)證

15、的重要性。其他科學(xué)用建造理論來(lái)保證正確性和可預(yù)見性。我們需要建造復(fù)雜系統(tǒng)可靠模型的理論和方法。異構(gòu)系統(tǒng)可能是同步的或異步的；不同的交互機(jī)制，如鎖閉、監(jiān)管、功能調(diào)用和消息傳達(dá)；執(zhí)行粒度不同，即硬件或軟件。我們需要從基于自動(dòng)機(jī)的組合中解放出來(lái)，考慮體系結(jié)構(gòu)的組合，像協(xié)議、調(diào)度和總線。我們需要研究某些特定的特性類，例如無(wú)死鎖、互操作。而不是去研究一般的安全特性。我們也需要研究特殊體系結(jié)構(gòu)的驗(yàn)證技術(shù)。體系結(jié)構(gòu)給定了部件間的交互機(jī)制。例如對(duì)環(huán)形或星形體系結(jié)構(gòu)，對(duì)帶搶先任務(wù)和固定優(yōu)先級(jí)的實(shí)時(shí)系統(tǒng)， 對(duì)時(shí)間觸發(fā)的體系結(jié)構(gòu)等。 可以像測(cè)試定義可測(cè)試性一樣，定義可驗(yàn)證性。總之，模型檢驗(yàn)已經(jīng)在硬件和軟件設(shè)計(jì)驗(yàn)證中

16、得到了應(yīng)用，但是，還有許多問題有待研究。模型檢驗(yàn)（結(jié)束語(yǔ)）（100101 ）學(xué)習(xí)完模型檢驗(yàn)(model checking)三位創(chuàng)建者的文章以后，現(xiàn)在可以說(shuō)幾句結(jié)束語(yǔ)了。科學(xué)大家就是科學(xué)大家。他們就模型檢驗(yàn)28 年來(lái)的發(fā)展，對(duì)歷史、研究動(dòng)機(jī)、已有成就及今后發(fā)展做了高度的概括和總結(jié)，指明了方向。但是，真要想做這方面的研究，還需要就其中的一個(gè)問題，查閱文獻(xiàn)，深入下去才行。當(dāng)今，在計(jì)算機(jī)工程與科學(xué)領(lǐng)域，困擾我們的一個(gè)問題是復(fù)雜性。系統(tǒng)很復(fù)雜，計(jì)算很復(fù)雜。但是，真要定義什么叫復(fù)雜，倒是一個(gè)很困難的問題。計(jì)算復(fù)雜性有一成套的理論，基于圖靈機(jī)可計(jì)算性，有所謂P 問題、 NP 問題。但是，實(shí)際上，一個(gè)多項(xiàng)式復(fù)

17、雜性的問題可能你算不了。例如解線性方程組是多項(xiàng)式復(fù)雜的，但是，13 億人建一個(gè)13 億階的方程組，可能現(xiàn)在的超級(jí)計(jì)算機(jī)也算不了。反過來(lái)，NP 難的問題，在IC 設(shè)計(jì)與測(cè)試領(lǐng)域比比皆是。SAT 就是一個(gè)典型的NP 難問題。對(duì)于特定的NP 問題，我們完全能夠用啟發(fā)式方法，得到很有效率的解。有些過去望而生畏的問題現(xiàn)在已經(jīng)有了有效的解。例如，OBDD （有序二進(jìn)制判決圖），測(cè)試生成，模型檢驗(yàn)等。本人.上世紀(jì)提出的布爾過程，由于復(fù)雜性問題而得不到響應(yīng)。但是，你想一想，我們現(xiàn)在IC 設(shè)計(jì)與測(cè)試中碰到的判決問題、優(yōu)化問題，哪一個(gè)是簡(jiǎn)單的。計(jì)算機(jī)發(fā)展到如此強(qiáng)大，不就是為了處理復(fù)雜問題的嗎？所以人類的智慧一定會(huì)越來(lái)越善于處理復(fù)雜問題。我想，如果我們請(qǐng)一位博士生，讀幾篇模型檢驗(yàn)的文章，然后寫一篇綜述，他一定會(huì)列出許多模型檢驗(yàn)工具，說(shuō)明它們有哪些功能。林林總