一種基于編碼的OBDD模型檢測的算法實現＊

馬曉龍 顧濱兵 劉鑫淼

（91404部隊 秦皇島 066000）

1 引言

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

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

2 模型檢測與OBDD

模型檢測的基本思想是用狀態遷移系統（S）如Kripke結構表示系統的行為，用模態／時序邏輯公式（F）如時序邏輯表達式CTL［1］描述系統的性質。這樣“系統是否具有所期望的性質”就轉化為數學問題“狀態遷移系統S是否是公式F的一個模型”，用公式表示為S｜＝F［4～5］。模型檢測的一般流程如圖1所示。

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

圖1 模型檢測的一般流程

3 微波爐驗證實例

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

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

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

圖2 微波爐狀態轉換模型

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

4 OBDD模型檢測的關鍵技術

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

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

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

圖3 微波爐狀態的BDD子樹

圖4 微波爐狀態編碼后的二叉判定子樹

關于轉換動作也可以用類似方法生成子二叉樹。基于編碼的BDD二叉判定樹的生成算法如下：

1）讀取狀態轉換模型，得到控制流圖Control-Graph；

2）讀取狀態個數；讀取轉換動作個數；

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

4）計算轉換邊個數，m＿TranNum；

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

｛根據控制流圖，得到轉換邊；

（1）轉換前狀態的二叉子樹生成；

（2）轉換動作的二叉子樹生成，并聯接到步驟（2）生成的子樹上；

（3）轉換后狀態的二叉子樹生成，并聯接到步驟（3）生成的子樹上｝

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

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

4.2 從BDD到OBDD的化簡算法

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

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

2）合并同構的子樹；

3）刪除多余的節點：

（1）刪除重復的終止節點；

（2）刪除重復的非終止節點；

（3）刪除沒必要存在的節點。

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

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

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

DelRepeatNode（）；／／／／／／刪除重復非終止結點及冗余結點；

3）執行函數DelRepeatNode（）

／／／兩兩查找重復非終止結點及冗余結點｝

①判斷是否是重復非終止結點

②結點的重新定向

③刪除重復結點｝

將當前層的上一層加入到臨時隊列m＿vTempOBDDList中

將當前層的上一層加入到臨時隊列vBread-NodeList中

4）for（i＝0；i＜層數；i＋＋）／／合并同構子樹｛

①對每一層節點，查找當層的其它節點

②對同層節點兩兩比較后繼節點，判斷是否是同構子樹

③對同構子樹的父節點重新定向｝

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

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

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

5 OBDD模型檢測的計算過程及算法實現

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

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

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

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

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

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

5.2 計算過程的具體實現

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

6 計算結果

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

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

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

終止節點為＊的表示能夠到達的狀態（該二叉樹可以表示4個狀態1、2、3、4），而終止節點為自然數的表示狀態集合為φ，因此可以看到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）的逐步及最終驗證結果

7 結語

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

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

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

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

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

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

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

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

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

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

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