一種基于編碼的OBDD模型檢測的算法實現(xiàn)＊

馬曉龍 顧濱兵 劉鑫淼

（91404部隊 秦皇島 066000）

1 引言

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

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

2 模型檢測與OBDD

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

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

圖1 模型檢測的一般流程

3 微波爐驗證實例

下面介紹一個常用的模型檢測實例，運用這個實例介紹OBDD模型檢測的基本思路和方法，并使用自己開發(fā)的模型檢測器MC＿OBDD對其進行了驗證。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.2 從BDD到OBDD的化簡算法

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.3 CTL公式的描述及模型檢測

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

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

5 OBDD模型檢測的計算過程及算法實現(xiàn)

5.1 利用CTL公式進行OBDD模型檢測的計算過程

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

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

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

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

5）對于EU的計算，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 計算過程的具體實現(xiàn)

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

6 計算結(jié)果

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

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

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

終止節(jié)點為＊的表示能夠到達的狀態(tài)（該二叉樹可以表示4個狀態(tài)1、2、3、4），而終止節(jié)點為自然數(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）的逐步及最終驗證結(jié)果

7 結(jié)語

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

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

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

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

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

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

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

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

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

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

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