基于切片技術的復雜模型驗證方法

紀明宇 于明霞 么一諾 畢曦文

(東北林業大學信息與計算機工程學院 黑龍江 哈爾濱 150040)

0 引 言

隨著科技發展的日新月異，計算機軟硬件系統趨于復雜化和抽象化使得其優劣性質驗證成為極為重要的內容。模型檢測作為一種能夠自動驗證并提出反例路徑的形式化驗證技術，已被廣泛應用于系統驗證。其基本思想是利用模型描述語言對已有系統進行建模，之后對該模型進行既定性質驗證，若滿足性質則進行下一項驗證，否則提出反例路徑。常用的形式化方法主要有線性時序邏輯(LTL)和計算樹邏輯(CTL)等[1]。典型的模型檢測工具有NuSMV[2]、SPIN[3]等?；ツM的引入使得LTL模型檢測能夠在驗證混合自動機時具有可判定性[4]。廣義CTL邏輯的討論能夠引發對模型檢測的更廣泛應用的思考[5]。目前在模型檢測領域，驗證技術已越來越成熟，其使用的手段如基于時序邏輯的規范化語言、自動機和不動點邏輯已為模型檢測領域的發展作出極大貢獻[6]。

狀態空間爆炸問題始終是模型檢測技術中需要解決的一大難點。在建立模型時所需考慮的狀態數量往往呈指數增長，最終難以控制模型的大小以致增大系統驗證的復雜度，解決該問題的思想包括狀態空間壓縮[7-8]、存儲空間壓縮的Hash Compact方法[9]、并行和分布式計算[10]、隨機化和啟發式搜索算法[11]等。近年來逐漸得到發展的限界模型檢測和切片技術等多種約減方法能夠在一定程度上解決有限馬爾可夫鏈的狀態爆炸問題。如：基于線性方程組求解的限界模型檢測算法在反例較短的情況下能夠快速完成檢測過程并避免空間爆炸[12]；基于懶惰切片提出的狀態空間搜索方法，在截斷狀態基礎上進行多次細化迭代，有效避免基于CEGAR的切片方法導致的重復計算[13]；基于狀態約減的信息攻防圖生成算法在實現目標網絡中主機覆蓋的基礎上描述了控制狀態空間組合爆炸問題的過程[14]；冗余路徑的點約減方法探究了有效簡化和優化USV在線路徑的相關問題[15]等。

然而，上述性質驗證和約減方法很少涉及對帶資源消耗的復雜遷移系統進行性質驗證。本文將在已有研究工作的基礎上，結合改進的圖的深度遍歷算法和概率矩陣的迭代運算，提出針對復雜模型的性質檢驗方法。首先利用棧的概念對系統進行初始的步數約束檢驗，對系統完成約減以避免冗余狀態和遷移的影響，再計算得出約減后的狀態間概率和資源消耗反例路徑，從而完成滿足帶資源消耗約束的直到性質驗證過程。

1 背 景

遷移系統在復雜系統的模型性質驗證領域，常用來作為模型來描述系統行為。

定義1遷移系統(TS)。遷移系統是基本的有向圖，其中點表示狀態，邊模仿遷移，即狀態變化。狀態描述了某個確定時間的系統行為的信息。遷移系統TS可以表示為元組T=(S,Act,→,AP,L),其中：S是狀態集合；Act是動作集合；→是遷移關系；AP是原子命題集合；標簽函數為L:S→2AP。

如果S、Act、AP有限，那么TS被稱為有限的遷移系統。由于基本的遷移系統模型在隨機性和確定性的表達能力上存在不足，所以出現了連續型和離散型的不同馬爾可夫模型用以描述待驗證的復雜隨機系統[16]。兩種模型分別具備描述在離散時間和連續任意時間的狀態遷移的能力,本文針對具有離散時間特征的系統模型展開研究。

例1DTMC舉例。

圖1為包含9個狀態的雙骰子投擲模型對應的不帶資源消耗的離散時間馬爾可夫模型。該模型描述了以下情形：投擲結果骰子數字和為7或11時為獲勝，系統遷移到達won狀態，骰子數字和在{2,3,12}中時到達last狀態，骰子數字和為其他結果時則記為“points”，并繼續投擲直到和為7時達到last狀態或和為“points”時達到won狀態。圖1模型忽略了各狀態所滿足的原子命題。

圖1 DTMC舉例

本文以DTMC為基礎,針對帶遷移資源消耗的離散時間馬爾可夫回報模型(DTMRC)展開研究。

定義3離散時間馬爾可夫回報模型(DTMRC)。DTMRC為五元組M=(S,P,L,AP,N,v)，其中：S、P、L、AP、v在定義2中已有說明；N:S×S→R≥0為遷移回報矩陣結構(R為遷移回報集合)，描述了從初始到各狀態的遷移資源；Ps1,n,s2=0.6表示從S1遷移到S2，發生遷移時所消耗的資源為n的概率為0.6。

例2DTMRC舉例。

圖2為帶有資源消耗的馬爾可夫模型,其包含8個狀態以及12個遷移過程。S0為初始狀態，包含原子命題{a,c}。對于狀態S0來說，在滿足原子命題a和c的條件下，下一步可遷移狀態集為{S1,S2,U}，發生遷移的概率分別為0.5、0.3和0.2，消耗的資源分別為10、10和15。

圖2 DTMRC舉例

DTMC模型一般可通過概率計算樹邏輯(PCTL)來描述驗證的性質。

定義4概率計算樹邏輯(PCTL)?；谠用}集合AP的PCTL狀態公式根據以下語法被形式化：φ::=true|a|φ1∧φ2|PJ(φ)。其中：a∈AP，φ是路徑公式；J?[0,1]是有理數界的中間值；PJ(φ)表示當前狀態滿足公式φ的概率值為J。

PCTL路徑公式可以根據以下語法被形式化：φ::=Oφ|φ1∪φ2|φ1∪≤nφ2，其中φ、φ1、φ2是狀態公式，Oφ表示最終進入滿足狀態公式φ，n∈N。

由于PCTL模型檢測的語法并不能描述遷移系統中資源消耗情況，所以對于DTMRC模型的性質，一些學者提出了改進的概率回報計算樹邏輯PRCTL[17]，它與PCTL的區別在于路徑公式的語義表達方式有所不同。

PRCTL的路徑公式表示為：

式中：n=[n1,n2]?R≥0和r=[r1,r2]?R≥0分別代表遷移步數和遷移資源消耗約束，U代表直到算子。

2 驗證過程

對于待驗證步數約束條件的DTMRC模型，可以將其看作帶有冗余的狀態和遷移的復雜系統。(1) 利用改進的圖的深度遍歷算法，得出符合步數的路徑集。針對進行模型檢測時反復出現的狀態爆炸問題，通過基于切片技術的約減方法來進行系統的縮減。首先將超過步數約束的遷移完全省去，實現一次約減；再檢查剩余的狀態是否包含在滿足直到條件的路徑中，若不包含則將這樣的狀態同時省去，實現二次約減，得到一個較為簡單的遷移系統。(2) 對于新的遷移系統構造各狀態間的遷移概率矩陣，進而通過概率迭代運算，計算出n步內a∪e的概率和。

定義5遷移系統概率矩陣迭代計算公式為：

X(i+1)=AX(i)+b0≤i≤n

X(0)=0i=0

式中：A表示為遷移系統的各狀態間初始概率矩陣；b表示為系統狀態到結束狀態的一步可達概率矩陣；X(i)表示為第i步的迭代后的概率矩陣。

例3n步可達概率計算舉例。

以圖1中的DTMRC模型為例，計算從狀態start到狀態won的n步內可達概率：

首先得出初始概率矩陣：

系統狀態到結束狀態won的一步可達概率矩陣：

然后對一步可達矩陣進行迭代，求解出兩步可達矩陣為：

三步可達矩陣為：

最后，基于資源消耗反例路徑的思想，根據每個遷移上所帶的資源數量，對已滿足概率條件和步數條件的遷移路徑，通過遍歷計算出各路徑的資源消耗以尋找反例集。若某路徑集的資源消耗和超過約束值，表示其為一個反例。

3 算法描述

本節對上節涉及的2個算法進行詳細說明：

算法1基于圖的路徑尋找算法getPaths

輸入：DTMRC模型M和步數約束m， 當前的起始節點cNode，當前起始節點的上一節點pNode，最初的起始節點sNode，中間節點需要滿足的原子命題a，最終節點需要滿足的原子命題e。

輸出：DTMRC模型M中所有滿足步數約束的路徑集。

getPaths(M,m,cNode,pNode,sNode,a,e){

1 nNode<-null;

2 n<-stack length;

/*找到路徑上的節點數*/

3 sNode╞a;

4 if(cNode !=null and pNode !=null and cNode==pNode)

/*出現環路*/

5 return false;

6 if(cNode !=null){

7 i<-0;

/*起始節點入棧*/

8 if(cNode╞e)

9 {if(n<=m+1)

10 showAndSavePath;

/*滿足步數的路徑轉儲并打印輸出*/ }

11 else{If(cNode╞a){

12 nNode<-cNode.getRelationNodes

/*從與cNode有連接關系的節點集中得到一個節點作為

下一次遞歸尋路時的起始節點*/

13 while(nNode !=null and nNode╞a){

14 if(pNode !=null and (nNode==sNode or nNode==pNode or isNodeInStack))

/*產生環路，重新尋找與cNode有連接關系的節點*/

15 {i++;

16 if(i>=cNode.getRelationNodes size)

17 nNode<-null;

18 else nNode<-cNode.getRelationNodes of i;

19 continue; }

20 if(getPaths(M,m,nNode,cNode,sNode,a,e))

/*遞歸調用*/

21 stack.pop();

/*找到路徑彈出棧頂節點*/

22 i++;

23 if(i>=cNode.getRelationNodes size)

24 nNode<-null;

25 else nNode<-cNode.getRelationNodes of I;

}}

26 stack pop;

27 return false; }}}

/*以cNode為起始節點到終點的路徑已經全部找到*/

28 else return false;}

/*算法結束*/

算法2面向資源消耗的反例路徑尋找算法getCE

輸入：PR[n]為存儲滿足步數約束和概率約束的路徑及其消耗資源數的結構體數組，R為資源消耗限制數。結構體為：

structlujing{

String P;

//把路徑上的狀態節點看成字符串

int r;}

//路徑消耗的資源數

輸出：反例路徑集及其消耗的資源和。

getCE(PR[n],R){

1 unsigned int sta=1;

2 inti,i1,i2,j,m=0,A[1000]={-1};

3 for(j=1;j<=(int)pow(2,n+1)-1;j++)

4 {for(i=0;i

5 {if((j&sta)!=0)

/*一條路徑與一個二進制位相對應，二進制位不為0對應

的路徑存在*/

6 {m=m+PR[i].r;

7 A[i1]=i;

/*記錄路徑在結構體數組的位置*/

8 i1++;}

9 sta=sta<<1;

/*sta對應的二進制加一*/}

10 if(m>=R)

11 {i1=0;

12 while(i1

13 {if(A[i1]!=-1)

14 {i2=A[i1];

15 printf(“%s”,PR[i2].P);}

16 i1++;}

17 printf(“%d”,m);}

18 m=0;i1=0;

19 A[1000]={-1};

20 sta=1;}

21 return 0;}

/*算法結束*/

算法1的時間復雜度主要與待驗證公式中的步數約束m有關，而算法2的時間復雜度主要與PR[n]結構體數組的大小有關。算法1為算法2提供了滿足步數約束的反例集。

4 實例分析

首先利用算法1進行步數條件的檢驗。得出滿足步數約束的路徑集{S0S2T1T4,S0S2T2T4,S0S1T1T4}。一步、兩步和三步遍歷過程如圖3、圖4和圖5所示。然后進行冗余狀態和遷移的二次約減，圖6為滿足步數約束的遷移圖，圖7為完成三步約減后的遷移系統。

圖3 一步遍歷過程

圖4 二步遍歷過程

圖6 滿足約束的遷移圖

圖7 三步約減后的遷移系統

針對新的遷移系統進行矩陣運算，求出從狀態S0到T4的3步之內可達且滿足a∪e的路徑概率。經計算可得S0到T4的3步可達概率為0.113，由此可知路徑集滿足概率小于等于0.2的條件。最后，利用算法2對圖7所示新的遷移系統進行資源消耗路徑集求解，把符合步數條件和概率條件的路徑集{S0S2T1T4,S0S2T2T4,S0S1T1T4}輸入，求得所消耗的路徑資源和為145。此時不滿足小于等于140的資源約束條件，則該路徑集為一個反例集合。

本文采用實驗對相應的方法進行了有效性驗證，實驗硬件環境為Intel(R) Core(TM) i5-7200U CPU @ 2.50 GHz 2.70 GHz，內存為8 GB。軟件環境包括操作系統為64位的Windows 7，編程軟件用MyEclipse 10.7。本文提出的方法可一定程度用于隨機分布式算法、安全協議分析等多個領域，用于以數學分析的角度進行可達性分析驗證。

5 結 語

本文對帶遷移資源消耗的復雜概率模型分步進行了可達性檢驗、概率檢驗和資源消耗檢驗，最終證明了基于帶資源消耗的復雜概率遷移系統的性質驗證方法的合理性和有效性。分析表明其能夠在一定程度上緩解狀態和遷移冗余的問題。未來的主要工作是面向更為龐大的遷移系統和更為復雜的性質檢驗，在狀態縮減和路徑壓縮等方法上展開進一步的研究。