紀(jì)明宇 于明霞 么一諾 畢曦文

(東北林業(yè)大學(xué)信息與計(jì)算機(jī)工程學(xué)院 黑龍江 哈爾濱 150040)

0 引 言

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

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

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

1 背 景

遷移系統(tǒng)在復(fù)雜系統(tǒng)的模型性質(zhì)驗(yàn)證領(lǐng)域，常用來(lái)作為模型來(lái)描述系統(tǒng)行為。

定義1遷移系統(tǒng)(TS)。遷移系統(tǒng)是基本的有向圖，其中點(diǎn)表示狀態(tài)，邊模仿遷移，即狀態(tài)變化。狀態(tài)描述了某個(gè)確定時(shí)間的系統(tǒng)行為的信息。遷移系統(tǒng)TS可以表示為元組T=(S,Act,→,AP,L),其中：S是狀態(tài)集合；Act是動(dòng)作集合；→是遷移關(guān)系；AP是原子命題集合；標(biāo)簽函數(shù)為L(zhǎng):S→2AP。

如果S、Act、AP有限，那么TS被稱為有限的遷移系統(tǒng)。由于基本的遷移系統(tǒng)模型在隨機(jī)性和確定性的表達(dá)能力上存在不足，所以出現(xiàn)了連續(xù)型和離散型的不同馬爾可夫模型用以描述待驗(yàn)證的復(fù)雜隨機(jī)系統(tǒng)[16]。兩種模型分別具備描述在離散時(shí)間和連續(xù)任意時(shí)間的狀態(tài)遷移的能力,本文針對(duì)具有離散時(shí)間特征的系統(tǒng)模型展開(kāi)研究。

例1DTMC舉例。

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

圖1 DTMC舉例

本文以DTMC為基礎(chǔ),針對(duì)帶遷移資源消耗的離散時(shí)間馬爾可夫回報(bào)模型(DTMRC)展開(kāi)研究。

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

例2DTMRC舉例。

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

圖2 DTMRC舉例

DTMC模型一般可通過(guò)概率計(jì)算樹(shù)邏輯(PCTL)來(lái)描述驗(yàn)證的性質(zhì)。

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

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

由于PCTL模型檢測(cè)的語(yǔ)法并不能描述遷移系統(tǒng)中資源消耗情況，所以對(duì)于DTMRC模型的性質(zhì)，一些學(xué)者提出了改進(jìn)的概率回報(bào)計(jì)算樹(shù)邏輯PRCTL[17]，它與PCTL的區(qū)別在于路徑公式的語(yǔ)義表達(dá)方式有所不同。

PRCTL的路徑公式表示為：

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

2 驗(yàn)證過(guò)程

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

定義5遷移系統(tǒng)概率矩陣迭代計(jì)算公式為：

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

X(0)=0i=0

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

例3n步可達(dá)概率計(jì)算舉例。

以圖1中的DTMRC模型為例，計(jì)算從狀態(tài)start到狀態(tài)won的n步內(nèi)可達(dá)概率：

首先得出初始概率矩陣：

系統(tǒng)狀態(tài)到結(jié)束狀態(tài)won的一步可達(dá)概率矩陣：

然后對(duì)一步可達(dá)矩陣進(jìn)行迭代，求解出兩步可達(dá)矩陣為：

三步可達(dá)矩陣為：

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

3 算法描述

本節(jié)對(duì)上節(jié)涉及的2個(gè)算法進(jìn)行詳細(xì)說(shuō)明：

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

輸入：DTMRC模型M和步數(shù)約束m， 當(dāng)前的起始節(jié)點(diǎn)cNode，當(dāng)前起始節(jié)點(diǎn)的上一節(jié)點(diǎn)pNode，最初的起始節(jié)點(diǎn)sNode，中間節(jié)點(diǎn)需要滿足的原子命題a，最終節(jié)點(diǎn)需要滿足的原子命題e。

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

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

1 nNode<-null;

2 n<-stack length;

/*找到路徑上的節(jié)點(diǎn)數(shù)*/

3 sNode╞a;

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

/*出現(xiàn)環(huán)路*/

5 return false;

6 if(cNode !=null){

7 i<-0;

/*起始節(jié)點(diǎn)入棧*/

8 if(cNode╞e)

9 {if(n<=m+1)

10 showAndSavePath;

/*滿足步數(shù)的路徑轉(zhuǎn)儲(chǔ)并打印輸出*/ }

11 else{If(cNode╞a){

12 nNode<-cNode.getRelationNodes

/*從與cNode有連接關(guān)系的節(jié)點(diǎn)集中得到一個(gè)節(jié)點(diǎn)作為

下一次遞歸尋路時(shí)的起始節(jié)點(diǎn)*/

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

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

/*產(chǎn)生環(huán)路，重新尋找與cNode有連接關(guān)系的節(jié)點(diǎn)*/

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))

/*遞歸調(diào)用*/

21 stack.pop();

/*找到路徑彈出棧頂節(jié)點(diǎn)*/

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為起始節(jié)點(diǎn)到終點(diǎn)的路徑已經(jīng)全部找到*/

28 else return false;}

/*算法結(jié)束*/

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

輸入：PR[n]為存儲(chǔ)滿足步數(shù)約束和概率約束的路徑及其消耗資源數(shù)的結(jié)構(gòu)體數(shù)組，R為資源消耗限制數(shù)。結(jié)構(gòu)體為：

structlujing{

String P;

//把路徑上的狀態(tài)節(jié)點(diǎn)看成字符串

int r;}

//路徑消耗的資源數(shù)

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

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)

/*一條路徑與一個(gè)二進(jìn)制位相對(duì)應(yīng)，二進(jìn)制位不為0對(duì)應(yīng)

的路徑存在*/

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

7 A[i1]=i;

/*記錄路徑在結(jié)構(gòu)體數(shù)組的位置*/

8 i1++;}

9 sta=sta<<1;

/*sta對(duì)應(yīng)的二進(jìn)制加一*/}

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;}

/*算法結(jié)束*/

算法1的時(shí)間復(fù)雜度主要與待驗(yàn)證公式中的步數(shù)約束m有關(guān)，而算法2的時(shí)間復(fù)雜度主要與PR[n]結(jié)構(gòu)體數(shù)組的大小有關(guān)。算法1為算法2提供了滿足步數(shù)約束的反例集。

4 實(shí)例分析

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

圖3 一步遍歷過(guò)程

圖4 二步遍歷過(guò)程

圖6 滿足約束的遷移圖

圖7 三步約減后的遷移系統(tǒng)

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

本文采用實(shí)驗(yàn)對(duì)相應(yīng)的方法進(jìn)行了有效性驗(yàn)證，實(shí)驗(yàn)硬件環(huán)境為Intel(R) Core(TM) i5-7200U CPU @ 2.50 GHz 2.70 GHz，內(nèi)存為8 GB。軟件環(huán)境包括操作系統(tǒng)為64位的Windows 7，編程軟件用MyEclipse 10.7。本文提出的方法可一定程度用于隨機(jī)分布式算法、安全協(xié)議分析等多個(gè)領(lǐng)域，用于以數(shù)學(xué)分析的角度進(jìn)行可達(dá)性分析驗(yàn)證。

5 結(jié) 語(yǔ)

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