馬曉龍 顧濱兵 劉鑫淼

（91404部隊(duì) 秦皇島 066000）

1 引言

模型檢測(cè)是一種被廣泛使用的驗(yàn)證有限狀態(tài)系統(tǒng)滿足規(guī)范的自動(dòng)化技術(shù)，它將形式化規(guī)范描述成命題時(shí)態(tài)邏輯包括LTL（線性時(shí)態(tài)邏輯）和CTL（分支時(shí)態(tài)邏輯）等，將系統(tǒng)（如電路設(shè)計(jì)、協(xié)議）模型化為狀態(tài)轉(zhuǎn)換系統(tǒng)，使用高效的搜索算法來判定規(guī)范是否在系統(tǒng)中成立［1～4］。

隨著被驗(yàn)證系統(tǒng)規(guī)模的不斷增大，狀態(tài)爆炸的問題在一定程度上制約時(shí)態(tài)邏輯模型檢測(cè)的進(jìn)一步發(fā)展，而有序二值判定圖（Ordered Binary Decision Diagrams）OBDD的使用，使基于 CTL及LTL的符號(hào)化模型檢測(cè)方法得到了極大突破，使驗(yàn)證規(guī)模有了明顯提高。雖然關(guān)于OBDD模型檢測(cè)方法的資料很多，但是國內(nèi)很少有關(guān)于OBDD模型檢測(cè)具體實(shí)現(xiàn)算法的介紹，本文將在由作者自行開發(fā)的 MC＿OBDD v1.0的基礎(chǔ)上介紹OBDD模型檢測(cè)工具的具體實(shí)現(xiàn)。

2 模型檢測(cè)與OBDD

模型檢測(cè)的基本思想是用狀態(tài)遷移系統(tǒng)（S）如Kripke結(jié)構(gòu)表示系統(tǒng)的行為，用模態(tài)／時(shí)序邏輯公式（F）如時(shí)序邏輯表達(dá)式CTL［1］描述系統(tǒng)的性質(zhì)。這樣“系統(tǒng)是否具有所期望的性質(zhì)”就轉(zhuǎn)化為數(shù)學(xué)問題“狀態(tài)遷移系統(tǒng)S是否是公式F的一個(gè)模型”，用公式表示為S｜＝F［4～5］。模型檢測(cè)的一般流程如圖1所示。

BDD［1，6～7］是 Bryant在1986年提出的一種基于圖形的二叉判定圖，是表示和操作布爾函數(shù)的有力工具。OBDD是化簡后的BDD。用OBDD驗(yàn)證分為三步：首先用表示狀態(tài)集合，然后用OBDD表示轉(zhuǎn)移關(guān)系，最后計(jì)算可達(dá)狀態(tài)。隨著基于OBDD表示的高效查找技術(shù)的發(fā)展，OBDD被應(yīng)用到知識(shí)表達(dá)和推理領(lǐng)域特別是符號(hào)化模型檢測(cè)領(lǐng)域中取得了很好的效果。

圖1 模型檢測(cè)的一般流程

3 微波爐驗(yàn)證實(shí)例

下面介紹一個(gè)常用的模型檢測(cè)實(shí)例，運(yùn)用這個(gè)實(shí)例介紹OBDD模型檢測(cè)的基本思路和方法，并使用自己開發(fā)的模型檢測(cè)器MC＿OBDD對(duì)其進(jìn)行了驗(yàn)證。

對(duì)一個(gè)微波爐工作的控制軟件，從系統(tǒng)建模開始說明它的驗(yàn)證過程。

微波爐的模型如圖2所示。

圖2 微波爐狀態(tài)轉(zhuǎn)換模型

上面的模型我們可以表示為M＝（S，S0，R，L，F(xiàn)）。要驗(yàn)證屬性用CTL公式表示，本例驗(yàn)證：公式AG（start→AFheat）是否滿足M。

4 OBDD模型檢測(cè)的關(guān)鍵技術(shù)

4.1 二叉判定圖BDD的編碼和生成

OBDD的模型檢測(cè)，首先要生成二叉判定圖BDD，本文使用二叉樹來表示BDD［8，10］。由圖2該微波爐用BDD的二叉判定子樹表示，如圖3所示。

圖3的左分支表示聯(lián)接變量節(jié)點(diǎn)的肯定命題、右分支表示聯(lián)接變量節(jié)點(diǎn)的否定命題。這種表示的好處是直接在子樹圖中可以直接找到各變量的取值，缺點(diǎn)是在很多情況下，該二叉子樹為稀疏二叉樹，節(jié)點(diǎn)數(shù)目過于龐大，為2m（m為變量數(shù)目），。本文采用對(duì)狀態(tài)編碼的方法，將狀態(tài)按照順序依次編為自然數(shù)1～n，并將其轉(zhuǎn)換成二進(jìn)制數(shù)，這樣就可以只使用k個(gè)布爾變量，其中k為不小于log2（n）的自然數(shù)，來生成二叉判定樹，生成的子樹為滿二叉樹或接近滿二叉樹，如圖4所示，大大壓縮了使用的空間。

圖3 微波爐狀態(tài)的BDD子樹

圖4 微波爐狀態(tài)編碼后的二叉判定子樹

關(guān)于轉(zhuǎn)換動(dòng)作也可以用類似方法生成子二叉樹?；诰幋a的BDD二叉判定樹的生成算法如下：

1）讀取狀態(tài)轉(zhuǎn)換模型，得到控制流圖Control-Graph；

2）讀取狀態(tài)個(gè)數(shù)；讀取轉(zhuǎn)換動(dòng)作個(gè)數(shù)；

3）GetBitLength（）；／／計(jì)算狀態(tài)和動(dòng)作的二進(jìn)制編碼所需布爾變量個(gè)數(shù)，生成狀態(tài)和動(dòng)作的二進(jìn)制數(shù)組；

4）計(jì)算轉(zhuǎn)換邊個(gè)數(shù)，m＿TranNum；

5）for（i＝0；i＜m＿TranNum；i＋＋）

｛根據(jù)控制流圖，得到轉(zhuǎn)換邊；

（1）轉(zhuǎn)換前狀態(tài)的二叉子樹生成；

（2）轉(zhuǎn)換動(dòng)作的二叉子樹生成，并聯(lián)接到步驟（2）生成的子樹上；

（3）轉(zhuǎn)換后狀態(tài)的二叉子樹生成，并聯(lián)接到步驟（3）生成的子樹上｝

圖5 微波爐模型生成的二叉判定樹

微波爐模型的控制流圖ControlGraph生成的BDD二叉樹如圖5所示。

4.2 從BDD到OBDD的化簡算法

一般由二叉判定樹形成OBDD，必須做以下工作進(jìn)行化簡：

1）保證所有路徑上變量出現(xiàn)的順序必須一致；

2）合并同構(gòu)的子樹；

3）刪除多余的節(jié)點(diǎn)：

（1）刪除重復(fù)的終止節(jié)點(diǎn)；

（2）刪除重復(fù)的非終止節(jié)點(diǎn)；

（3）刪除沒必要存在的節(jié)點(diǎn)。

對(duì)于（1），可以從4.1節(jié)看到，路徑上變量出現(xiàn)的順序是一致的，而對(duì)于3）-（1），4.1節(jié)的生成過程以連接到true和false為結(jié)束，所以也不存在重復(fù)的終止節(jié)點(diǎn)。所以化簡過程重點(diǎn)在于刪除重復(fù)的非終止節(jié)點(diǎn)和冗余節(jié)點(diǎn)，以及合并同構(gòu)子樹，化簡算法描述如下：

1）獲取最下一層的節(jié)點(diǎn)加入隊(duì)列vBreadNodeList；

2）while（vBreadNodeList［i］的左兒子或右兒子不為空）

DelRepeatNode（）；／／／／／／刪除重復(fù)非終止結(jié)點(diǎn)及冗余結(jié)點(diǎn)；

3）執(zhí)行函數(shù)DelRepeatNode（）

／／／兩兩查找重復(fù)非終止結(jié)點(diǎn)及冗余結(jié)點(diǎn)｝

①判斷是否是重復(fù)非終止結(jié)點(diǎn)

②結(jié)點(diǎn)的重新定向

③刪除重復(fù)結(jié)點(diǎn)｝

將當(dāng)前層的上一層加入到臨時(shí)隊(duì)列m＿vTempOBDDList中

將當(dāng)前層的上一層加入到臨時(shí)隊(duì)列vBread-NodeList中

4）for（i＝0；i＜層數(shù)；i＋＋）／／合并同構(gòu)子樹｛

①對(duì)每一層節(jié)點(diǎn)，查找當(dāng)層的其它節(jié)點(diǎn)

②對(duì)同層節(jié)點(diǎn)兩兩比較后繼節(jié)點(diǎn)，判斷是否是同構(gòu)子樹

③對(duì)同構(gòu)子樹的父節(jié)點(diǎn)重新定向｝

4.3 CTL公式的描述及模型檢測(cè)

CTL可以描述狀態(tài)的前后關(guān)系和分枝情況，描述一個(gè)狀態(tài)的基本元素是原子命題符號(hào)。公式由原子命題，邏輯連接符和模態(tài)算子組成。CTL的邏輯連接符包括：﹁（非），∨（或），∧（與），它的模態(tài)算子包括：E（Exists），A（Always），X（Nexttime），U（Until），F(xiàn)（Future），G（Global）。可以證明所有CTL公式都可用﹁、∨、EX、EG、EU來表示。

本質(zhì)上，本模型檢測(cè)方法進(jìn)行驗(yàn)證的過程是按照CTL公式用舊OBDD計(jì)算新OBDD的過程。驗(yàn)證時(shí)，我們從被驗(yàn)證公式的最深層的子公式開始驗(yàn)證，一級(jí)一級(jí)逐步擴(kuò)展到驗(yàn)證整個(gè)公式。

5 OBDD模型檢測(cè)的計(jì)算過程及算法實(shí)現(xiàn)

5.1 利用CTL公式進(jìn)行OBDD模型檢測(cè)的計(jì)算過程

1）對(duì)于﹁f運(yùn)算，我們只需復(fù)制f的OBDD并將其中終止節(jié)點(diǎn)的值交換即可；

2）對(duì)于f∨g運(yùn)算，如果f、g是用二叉判定樹表示的，我們要找到滿足f∨g的狀態(tài)，只需按先根次序同時(shí)遍歷f、g的二叉判定樹，一邊遍歷一邊生成一個(gè)新的二叉判定樹，然后對(duì)同一個(gè)狀態(tài)在兩個(gè)二叉判定樹的終止節(jié)點(diǎn)的值進(jìn)行析取運(yùn)算，把所得值標(biāo)在新二叉判定樹中，就可以判斷哪些狀態(tài)滿足f∨g，OBDD是化簡后的二叉判定樹；

3）對(duì)于EX的計(jì)算，EXf表示一個(gè)狀態(tài)的下一個(gè)狀態(tài)滿足f。我們可以遍歷S的OBDD，遍歷到狀態(tài)s的終止節(jié)點(diǎn)時(shí)，通過查找R的OBDD可以找到s的所有后繼狀態(tài)，然后根據(jù)f的OBDD就能得知這些后繼狀態(tài)中是否有滿足f的狀態(tài)，若有，則s滿足EXf，這樣當(dāng)遍歷完整個(gè)S的OBDD時(shí)，就能得知哪些狀態(tài)滿足EXf，得到所求的OBDD；

4）對(duì)于EG的計(jì)算，EGf＝f∧EX（EGf），我們可以遍歷S的OBDD，找出所有滿足f的狀態(tài)，構(gòu)成集合S′，如果一個(gè)狀態(tài)滿足EGf，那么它的某個(gè)后繼也一定滿足f并在S′中，如果它的所有后繼都不在S′中，那么它一定不滿足EGf，應(yīng)該從S′中刪除它，反復(fù)刪除這樣的狀態(tài)，直到S′不再發(fā)生變化；

5）對(duì)于EU的計(jì)算，E［f1∪f2］＝f2∨（f1∧EX（E［f1∪f2］）），我們可以遍歷S的OBDD，找出所有滿足f2的狀態(tài)，構(gòu)成集合S′，然后再找出這些狀態(tài)的前驅(qū)狀態(tài)，把其中滿足f1的添加到S′中，然后再找新添加的狀態(tài)的前驅(qū)狀態(tài)，把其中滿足f1的狀態(tài)添加到S′中，如此反復(fù)，直到S′不再變化為止。

5.2 計(jì)算過程的具體實(shí)現(xiàn)

由于篇幅所限，我們只給出f∨g的OBDD計(jì)算如下：

6 計(jì)算結(jié)果

對(duì)第4節(jié)給出的例子，我們來驗(yàn)證公式AG（start→AFheat）是否滿足M。

首先利用5.1給出公式的轉(zhuǎn)換公式：﹁E（trueUstart∧EG（﹁heat））

我們逐步給出公式各部分的驗(yàn)證結(jié)果，最后給出最終結(jié)果如圖6所示。

終止節(jié)點(diǎn)為＊的表示能夠到達(dá)的狀態(tài)（該二叉樹可以表示4個(gè)狀態(tài)1、2、3、4），而終止節(jié)點(diǎn)為自然數(shù)的表示狀態(tài)集合為φ，因此可以看到S（EG（﹁heat））＝｛1，2，3｝，S（S∧EG（﹁heat））＝｛2｝，S（E（trueUstart∧EG（﹁heat）））＝｛1，2，3，4｝，S（﹁E（trueUstart∧EG（﹁heat）））＝φ。因此公式AG（start→AFheat）不滿足M。

圖6 AG（start→AFheat）的逐步及最終驗(yàn)證結(jié)果

7 結(jié)語

雖然近些年來，模型檢測(cè)是人工智能方面的一個(gè)研究熱點(diǎn)，對(duì)模型檢測(cè)和OBDD技術(shù)的介紹也很多，但是很少有關(guān)于OBDD模型檢測(cè)實(shí)現(xiàn)算法的相關(guān)介紹，作者通過介紹自行開發(fā)的OBDD模型檢測(cè)器，給出了基于編碼的OBDD模型檢測(cè)的具體實(shí)現(xiàn)算法，并利用該模型檢測(cè)器驗(yàn)證了一個(gè)例子，填補(bǔ)了這一空白，并在今后的工作中逐步完善。

［1］BRYANT R E.Graph based algorithms for Boolean function manipulation［J］.IEEE Transactions on Computers，1986（8）：677～691

［2］林惠民，張文輝.模型檢測(cè)：理論、方法與應(yīng)用［J］，電子學(xué)報(bào)，2002，12（30）：1907～1910

［3］蘇開樂，駱翔宇，呂關(guān)鋒.符號(hào)化模型檢測(cè)CTL［J］.計(jì)算機(jī)學(xué)報(bào)，2005，11（28）：1978～1979

［4］徐暢，劉吉鋒，孫吉貴.基于經(jīng)典邏輯的安全協(xié)議模型檢測(cè)算法［J］.計(jì)算機(jī)科學(xué)，2008，6（35）：20

［5］趙輝，李彤.基于模型的驗(yàn)證及其方法［J］.計(jì)算機(jī)工程，2001，8（27）：45～56

［6］呂關(guān)鋒，蘇開樂，等.基于BDD的圖表示及其算法［J］.中山大學(xué)學(xué)報(bào)（自然科學(xué)版），2006，1（45）：20

［7］郭建，杜建敏，等.基于時(shí)態(tài)邏輯的硬件設(shè)計(jì)形式化驗(yàn)證技術(shù)－模型檢驗(yàn)［J］.小型微型計(jì)算機(jī)系統(tǒng)，2001，5（22）：521～523

［8］王飛明，胡元闖，董榮勝.模型檢測(cè)研究進(jìn)展［J］.廣西科學(xué)院學(xué)報(bào)，2008，24（4）：320～321

［9］劉林霞，張自強(qiáng)，何安平.基于模型檢測(cè)的半結(jié)構(gòu)化數(shù)據(jù)查詢［J］.計(jì)算機(jī)與數(shù)字工程，2009，37（8）

［10］賀亞博，郝克剛，葛瑋.模型檢測(cè)在軟件需求分析及設(shè)計(jì)中的應(yīng)用［J］.計(jì)算機(jī)應(yīng)用與軟件，2009，4（26）：129