郎大鵬，黃少濱，程媛，遲榮華

(哈爾濱工程大學，計算機科學與技術(shù)學院，黑龍江哈爾濱150001)

模型檢測技術(shù)［1］由于能在驗證過程中自動生成反例，因此被廣泛應用于硬件系統(tǒng)、多Agent系統(tǒng)、通訊協(xié)議和嵌入式系統(tǒng)等有限狀態(tài)并發(fā)系統(tǒng)的驗證中［2］。為了解決驗證過程中的狀態(tài)空間爆炸問題，抽象技術(shù)［3-4］被認為是最常用且可行的方法。然而抽象導致了偽反例的出現(xiàn)，當抽象模型不滿足性質(zhì)時，需要檢查該反例是否為偽反例。如果反例不對應具體模型中任何的路徑，則產(chǎn)生了偽反例，需要對抽象模型進行精化［5-6］。實踐中，反例往往不止一條并且存在交互，反例精化過程則需要對所有路徑進行窮舉遍歷，對時間和空間有較高要求。由模型檢測帶來的性能提升有時會被復雜的反例分析過程消耗［7］。并且當由于時間空間原因不得不停止精化算法時，反例結(jié)果既不完備，也無法為設(shè)計人員提供關(guān)于反例的具體信息。針對此問題，本文提出基于關(guān)鍵反例的提取精化算法。

1 研究背景

1.1 模型檢測及抽象

模型檢測用自動機表示程序或數(shù)字電路的遷移結(jié)構(gòu)，用基于LTL或CTL語言表示斷言或需要滿足的規(guī)范，通過遍歷自動機上所有的狀態(tài)驗證邏輯公式的可滿足性。E.M.Clark［5］提出的存在性抽象框架理論奠定了符號模型檢測的基礎(chǔ)。文獻［6］中討論了基于等價關(guān)系和存在熵的構(gòu)建抽象技術(shù)，避免了構(gòu)建全局的具體狀態(tài)空間。文獻［7］通過在反例狀態(tài)空間中添加額外信息，如距離矩陣，比較特定反例間的距離，作為搜索最近證例的互模擬方法［8］。這2種方法都存在搜索域過大，變量值過多的問題，因此效率較低。文獻［9］中提出了反例引導的抽象精化方法，迭代地用基于OBDD的符號模型檢測對模型和斷言的滿足性判斷，圖1中給出了模型檢測及精化過程流程。

1.2 Kripke結(jié)構(gòu)和ACTL*

本文采用具有完備操作的［5］CTL*的一個子集ACTL*表示斷言，即時序操作符只存在A，且﹁操作符只作用在原子公式上。反例可表示為［6］:TS|≠?φ，其中φ是任意的ACTL*公式。對于單一路徑上的反例，記作:TS|≠?φ。針對常量斷言來說ACTL*公式AGp和LTL公式Gp在狀態(tài)遷移中表達相同的含義且解析復雜度相同［5］。

定理1顯式狀態(tài)模型檢測中，基于CTL的模型檢測的時間復雜度為O(|M||φ| ) ，其中為模型中狀態(tài)數(shù)為斷言中包含原子命題數(shù)［5］。

1.3 節(jié)點重要性評價

在計算反例和抽象的算法中，常常需要基于遷移圖的強連通性質(zhì)計算節(jié)點最弱前置條件［11］，文獻［12］中提出網(wǎng)絡中具有K-核值最大的節(jié)點為系統(tǒng)中起到傳播功能最重要的節(jié)點。但是在Autonomous System網(wǎng)絡中［13］，K-核為1的節(jié)點比例占37.97%，度為1的節(jié)點比例占36.89%，介數(shù)為0的節(jié)點比例為52.47%。文中設(shè)計了結(jié)合具體遷移系統(tǒng)結(jié)構(gòu)的模型中節(jié)點權(quán)重算法，計算模型中節(jié)點權(quán)值。

圖1 模型檢測流程圖Fig.1 Model checking flow diagram

2 狀態(tài)權(quán)重計算

2.1 關(guān)鍵節(jié)點

由邏輯語義抽象的模型M^，空間復雜度通常比原模型M呈指數(shù)型改進［12］，但是當為實際應用系統(tǒng)建模時，如果不對系統(tǒng)節(jié)點的重要性進行區(qū)分，就無法更有針對性地進行檢測。當出現(xiàn)以下情況時，認為節(jié)點是“重要”的，如圖2所示。

圖2 關(guān)鍵狀態(tài)節(jié)點示意圖Fig.2 Key state node diagram

1)狀態(tài)si有多個前驅(qū)及后繼節(jié)點，如圖2(a)中s7鄰接節(jié)點個數(shù)最多，因此s7是重要的;

2)狀態(tài)si是循環(huán)的初始節(jié)點，如圖2(b)中節(jié)點s3;

3)狀態(tài)si是2個狀態(tài)子圖的橋節(jié)點，如圖2(c)中的s5;

4)狀態(tài)si是證例和反例的分支狀態(tài)，如圖2(d)中，〈s2，s3，s4，s5，s7，s8〉為反例路徑〈s2，s10，s12，s8〉為證例路徑，其中狀態(tài)節(jié)點s2為分支節(jié)點，因此權(quán)重更高。

2.2 評價指標

一個狀態(tài)遷移圖表示為一個有向圖TS=〈V，E〉，其中TS是一個有向連通圖，V=〈v1，v2，…，vm〉是圖中節(jié)點集合，包含m個節(jié)點是圖中邊的集合，包含n條邊，有E?V×V。有向圖TS的鄰接矩陣ATS的元素為sij∈{0，1}表示有向圖中表示狀態(tài)的節(jié)點i到j的有向邊，對應于狀態(tài)遷移圖TS中從si到sj的一個遷移，單位列向量記為:el=［e1e2… en］T，其中ei=1(1≤i≤n)，則定義

定義1:節(jié)點i的單一權(quán)重計算如下:

定義2:連接節(jié)點i和節(jié)點j的邊的權(quán)重定義為節(jié)點i和節(jié)點j的單一權(quán)重的積，記作:

定義3:節(jié)點i的整體權(quán)重，定義為連接該節(jié)點的邊的權(quán)值的和，記作:

其中Γi為節(jié)點i的出射和入射鄰居節(jié)點集合。

為了規(guī)范在狀態(tài)空間爆炸下有向圖的節(jié)點權(quán)值范圍，需要對節(jié)點權(quán)重進行歸一化計算，公式如下:

下面給出了計算系統(tǒng)遷移圖中重要狀態(tài)節(jié)點權(quán)重的算法:

3 抽象函數(shù)

3.1 抽象

本節(jié)中基于Kripke結(jié)構(gòu)，設(shè)vi∈V為系統(tǒng)變量，用中⊥表示該值未定義，任意變量賦值表示為Evi= {vi=d|d∈D∪{ ⊥ } }。本文將抽象帶權(quán)模型記作

定義4 設(shè)A為一組斷言集，存在si∈S和sj∈S，對于所有的ρ∈A，當且僅當si|=ρ成立時，sj|=ρ成立，相應的可以表示為hρ(si)=hρ(sj)，簡記為:，稱hρ()是A上的抽象函數(shù)。

3.2 帶有權(quán)重的抽象算法

在以往研究中［4-5］，人工選取可見的狀態(tài)變量集Vvisible和不可見的程序變量集 Vinvisible效率較低。本節(jié)基于狀態(tài)節(jié)點在遷移圖中權(quán)重，篩選出集合Vvisible={Vv|Vv?VVinvisible}。算法2通過給定一個原始模型K，首先根據(jù)Vvisible，計算Kw;其中，根據(jù)權(quán)重閾值的比較，將關(guān)鍵節(jié)點抽取到集合Visible［］中，用于構(gòu)造Kripke結(jié)構(gòu)。

由于狀態(tài)節(jié)點在不同應用環(huán)境中權(quán)重值取值范圍較大。在給定的帶權(quán)的Kripke模型Kw下，抽象過程需要保證:1)初始狀態(tài)集I中非空子集經(jīng)過抽象后為抽象后模型中初始狀態(tài)集I^中的狀態(tài);2)抽象關(guān)系非空;3)滿足的斷言即原子命題集是完備的;4)新狀態(tài)變量集合為calVisible()計算得到的。下面給出計算帶有權(quán)重的Kripke模型算法。

文獻［6，10］中給出對抽象模型進行精化的方法，迭代地對新抽象模型進行模型檢測，直到證明系統(tǒng)是safe的或者找到真實狀態(tài)反例路徑。

4 偽反例

4.1 偽反例產(chǎn)生原理

圖3系統(tǒng)遷移圖中包含27個狀態(tài)，根據(jù)算法SplitPath，將該系統(tǒng)劃分為包含3個狀態(tài)的抽象模型，由圖中所示，反例路徑為〈s1，s3，s4，s6，s7，s10〉，經(jīng)分析，反例路徑中遷移→，是偽反例，因為原模型中路徑不能遷移到中的任意狀態(tài)中，即

圖3 失敗狀態(tài)示意圖Fig.3 Failure state diagram

4.2 基于狀態(tài)權(quán)重的偽反例定位

當沒有后繼的狀態(tài)和沒有前驅(qū)的狀態(tài)被抽象算法劃分到同一個抽象狀態(tài)中，在抽象模型中產(chǎn)生了新的遷移，導致偽反例的出現(xiàn)，給這2種狀態(tài)分別命名:

1)終止狀態(tài)sd:存在一條從s0到sd的遷移，且sd無后繼狀態(tài);

2)錯誤狀態(tài)sb:不存在從s0到s0的遷移，且s0有后繼狀態(tài);

定理2 在同一個狀態(tài)簇(抽象狀態(tài))中，同時存在終止狀態(tài)和錯誤狀態(tài)，則該抽象狀態(tài)位于一條偽反例路徑。因此，精化算法需驗證任意一個抽象狀態(tài)中不同時包含終止狀態(tài)和錯誤狀態(tài)。

當存在某個抽象狀態(tài)集中，存在以下情況時，則說明可能產(chǎn)生了偽反例，即

算法首先過濾出符合上面條件的狀態(tài)集。如果Reachable(sj)成立，則該反例為偽反例;反之，如圖4所示，抽象狀態(tài)中包含s4和s5，其中s4的出度Dout=0且Reachable(s4)=TRUE;雖然≠0，但其直接前驅(qū)s3為初始狀態(tài)不可達，因此需要進一步計算狀態(tài)的前驅(qū)和后繼狀態(tài)關(guān)系。

圖4 偽反例路徑示例Fig.4 An example of spurious counterexample path

如下給出檢測偽反例算法:

4.3 定位關(guān)鍵反例

其中:

第5節(jié)實驗中給出本算法的并行版本，并證明其效率獲得較大的提升。

5 實驗

本文將文獻［3］中的算法SplitPath與論文中的算法checkKeycounterexampel()進行了比較。實驗服務器為Intel雙核2.4 GHz，GNU/Linux(Ubuntu 12)，16 G RAM。實驗程序集選自BLAST［http:// mtc.epfl.ch/software-tools/blast/index-epfl.php］以及SYC M C http://www.ccellera.rg/ownloads/ standards/sy stemc/］補充，分別是精簡Windows NT device drivers 64 bit，以及System C程序。實驗結(jié)果如圖5所示。

圖5 算法效率對比Fig.5 Algorithm efficiency comparison

6 結(jié)論

本文給出了抽象狀態(tài)權(quán)重的計算方法，同時提出包含權(quán)重高的抽象狀態(tài)的反例比其他反例更重要。關(guān)鍵反例可能在錯誤定位和向設(shè)計者提供更豐富關(guān)于狀態(tài)遷移系統(tǒng)結(jié)構(gòu)中起到更關(guān)鍵的作用。

目前，模型檢測已被用于軟硬件以外的領(lǐng)域。如公共政策分析，定位關(guān)鍵反例即找到違反公共政策的關(guān)鍵狀態(tài)節(jié)點;在法律執(zhí)行領(lǐng)域，當進行案件判決或出現(xiàn)錯判誤判時，關(guān)鍵反例可以成為問詢的依據(jù)。將“關(guān)鍵反例”的識別和計算，逐步從海量信息中提取關(guān)鍵信息是未來的一個發(fā)展方向。

［1］CLARKE E M，EMERSON E A.Design and synthesis of synchronization skeletons using branching time temporal logic［C］//KOZEN D.Logics of Programs:Workshop，Yorktown Heights，New York，USA，1982，131:52-71.

［2］CLARKE E M，GRUMBERG O，PELED D A.Model Checking［M］.Boston:The MIT Press，2000:27-108.

［3］PODELSKI A，RYBALCHENKO A.ARMC:the logical choice for software model checking with abstraction refinement［M］.HANUS M.Practical Aspects of Declarative Languages.Berlin:Springer，2007，4354:245-259.

［4］ABDULLA R A，ANNICHINI A，BENSALEM S，et al.Verification of infinite-state systems by combining abstraction and reachability analysis［M］.HALBWACHS N，PELED D.Computer-Aided Verification.Beilin:Springer， 1999，1633:146-159.

［5］CLARKE E，GRUMBERG O，JHA S，et al.Counterexample-guided abstraction refinement for symbolic model checking［J］.Journal of the ACM，2003，50(5):752-794.

［6］曾紅衛(wèi)，繆淮扣.構(gòu)件組合的抽象精化驗證［J］.軟件學報，2008，19(5):1149-1159.

ZENG Hongwei，MIAO Huaikou.Verification of component composition based on abstraction refinement［J］.Journal of Software，2008，19(5):1149-1159.

［7］CLARKE E M，GUPTA A，STRICHMAN O.SAT-Based Counterexample-guided abstraction refinement［J］.IEEE Transactions on computer aided design，2004，23(7): 1113-1123.

［8］GROCE A.Error explanation with distance metrics［M］.JENSEN K，PODELSKI A.Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer，2004:108-122.

［9］BEER I，BEN-DAVID S，CHOCKLER H，et al.Explaining counterexamples using causality［J］.Formal Methods in System Design，2012，40(1):20-40.

［10］GROCE A，KROENING D，LERDA F.Understanding counterexamples with explain［J］.Computer Aided Verification，Springer，2004:453-456.

［11］FREEMAN L C，ROEDER D，MULHOLLAND R R.Centrality in social networks:II.Experimental results［J］.Social Networks，1979-1980，2(2):119-141.

［12］NEWMAN M E J.A measure of betweenness centrality based on random walk［J］.Social Networks，2005，27 (1):39-54.