洪云端，李永明

(1.陜西師范大學(xué) 計(jì)算智能實(shí)驗(yàn)室，陜西 西安 710119；2.陜西師范大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院，陜西 西安 710119)

0 引 言

模型檢測(cè)[1-3]作為一種形式化驗(yàn)證工具，主要包含三個(gè)步驟：建立模型，描述系統(tǒng)性質(zhì)，使用模型檢測(cè)算法驗(yàn)證系統(tǒng)是否滿足這些性質(zhì)。系統(tǒng)模型通常使用布爾傳遞系統(tǒng)模型或者Kripke結(jié)構(gòu)，系統(tǒng)性質(zhì)則通過(guò)時(shí)序邏輯進(jìn)行刻畫，最終驗(yàn)證結(jié)果會(huì)給出一個(gè)布爾結(jié)果，滿足性質(zhì)給出是，不滿足性質(zhì)系統(tǒng)會(huì)給出否，并且給出反例。模型檢測(cè)廣泛應(yīng)用于許多重要的系統(tǒng)，例如SPIN[4]，NuSMV[5]。

模型檢測(cè)器受制于經(jīng)典邏輯，有許多問(wèn)題在經(jīng)典邏輯上無(wú)法解決，例如現(xiàn)實(shí)生活當(dāng)中的不確定性[6]。當(dāng)處理這些信息的時(shí)候，傳統(tǒng)的模型檢測(cè)器便失去了作用。其中非經(jīng)典多值邏輯提供了一種很好的解決方法來(lái)處理信息的不確定性和不完備性，例如文獻(xiàn)[7]提出的用三值邏輯去解釋模型檢測(cè)的結(jié)果，文獻(xiàn)[8]使用四值邏輯對(duì)門級(jí)電路的抽象模型進(jìn)行推理驗(yàn)證。

文獻(xiàn)[9]提出基于多值可能性測(cè)度的多值計(jì)算樹邏輯的模型檢測(cè)，解決了在系統(tǒng)中存在“是”和“否”之間狀態(tài)的邏輯問(wèn)題，其采用兩種方式：第一，將系統(tǒng)中狀態(tài)解釋為多值的；第二，將系統(tǒng)中狀態(tài)之間的轉(zhuǎn)移關(guān)系也設(shè)置為多值的。

基于文獻(xiàn)[10]，文中設(shè)計(jì)了自動(dòng)化驗(yàn)證的多值模型檢測(cè)器。首先，對(duì)構(gòu)建的多值模型Kripke結(jié)構(gòu)，從計(jì)算機(jī)存儲(chǔ)的方面進(jìn)行數(shù)據(jù)結(jié)構(gòu)上的設(shè)計(jì)，并且分析了時(shí)間復(fù)雜度，盡量用最優(yōu)化的結(jié)構(gòu)對(duì)狀態(tài)和轉(zhuǎn)移函數(shù)進(jìn)行存儲(chǔ)，使模型檢測(cè)器能夠計(jì)算更多的狀態(tài)；其次，設(shè)計(jì)了模型檢測(cè)器的框架，從輸入的模型以及性質(zhì)，如何轉(zhuǎn)換模型和性質(zhì)，如何對(duì)性質(zhì)進(jìn)行計(jì)算，到完成模型檢測(cè)后如何輸出檢測(cè)結(jié)果，并對(duì)時(shí)間復(fù)雜度進(jìn)行了分析。

1 多值可能性測(cè)度下的模型檢測(cè)

1.1 多值可能性Kripke結(jié)構(gòu)

定義1[11]：設(shè)(l，≤)是偏序集，若l中任意兩個(gè)元素都存在上確界以及下確界，則稱(l，≤)是格，為了方便，這樣的格稱為偏序格。

定義2[12]：一個(gè)多值Kripke結(jié)構(gòu)是一個(gè)五元組M=(S,P,I,AP,L)，其中:

S是一個(gè)可數(shù)、非空的狀態(tài)集合；

P:S×S→l表示多值傳遞關(guān)系；

I:S→l是初始分布函數(shù)；

AP是原子命題的集合；

L:S×AP→l是一個(gè)標(biāo)簽函數(shù)。

注：多值傳遞函數(shù)P:S×S→l可以通過(guò)l格值表示，將這個(gè)矩陣表示為P。矩陣P傳遞閉包，表示為P+。矩陣P的自反和傳遞閉包用P*表示，P*=P0∨P+。Paths(M)表示M中所有路徑的集合。

定義3[13]：一個(gè)多值Kripke結(jié)構(gòu)M，其函數(shù)PoM:Paths(M)→l定義如下：

對(duì)任意π=s0s1…∈Paths(M)，有如下定義函數(shù)：

PoM:2Paths(M)→l

PoM稱為在Ω=2Paths(M)上的廣義可能性測(cè)度。

定義4[14]：對(duì)于一個(gè)多值Kripke結(jié)構(gòu)M，定義一個(gè)函數(shù)rP:S→l，表示在M上從初始狀態(tài)s出發(fā)的最大可能性路徑：

rP(s)=∨{P(s,s1)∧P(s1,s2)∧…|s1,

s2,…∈S}

其中計(jì)算rP(s)的方法依據(jù)定理1。

定理1[15]：一個(gè)有限多值Kripke結(jié)構(gòu)M，M中的一個(gè)狀態(tài)s，有：

rP(s)=∨{P+(s,t)∧P+(t,t)|t∈S}

使用矩陣表示為：

rP(s)=P+°D

其中，符號(hào)“°”表示sup-inf合成運(yùn)算。

1.2 基于多值可能性測(cè)度的多值計(jì)算樹邏輯

引入一種新的定量時(shí)序邏輯對(duì)性質(zhì)進(jìn)行描述，即可能性測(cè)度上的多值計(jì)算樹邏輯。

定義5[16](MvCTL語(yǔ)構(gòu))：多值CTL(簡(jiǎn)稱MvCTL)關(guān)于原子命題AP的狀態(tài)公式：

Φ::r|α|Φ1∧Φ2|Φ|Po(φ)

其中，α∈AP,r∈l，φ是MvCTL路徑公式，如下：

φ::=OΦ|Φ1∪Φ2|Φ1∪≤nΦ2|□Φ

其中Φ,Φ1和Φ2是狀態(tài)公式并且n∈N。

定義6(MvCTL語(yǔ)義)：多值Kriple結(jié)構(gòu)M=(S,P,I,AP,L)，a∈AP是原子命題，s∈S表示狀態(tài)，Φ,Ψ是MvCTL狀態(tài)公式，φ是MvCTL路徑公式。對(duì)公式Φ，其語(yǔ)義是格值模糊集‖Φ‖:S→l，對(duì)任意s∈S，r∈l，其定義如下：

‖r‖(s)=r

‖a‖(s)=L(s,a)

‖Φ∧Ψ‖(s)=‖Φ‖(s)∧‖Ψ‖(s)

‖Po(φ)‖(s)=Po(s|=φ)

對(duì)于路徑公式φ，其語(yǔ)義是一個(gè)格值模糊集‖φ‖:Paths(M)→l，其定義如下：

‖OΦ‖(π)=‖Φ‖(π[1])

‖Φ∪Ψ‖(π)=∨j≥0∧k

Φ∪≤nΨ‖(π)=∨j≤n∧k

路徑公式◇Φ(最終的)有如下語(yǔ)義：

2 多值可能性模型檢測(cè)算法

MvCTL模型檢測(cè)的問(wèn)題可以描述如下：

給一個(gè)有限廣義的多值Kripke結(jié)構(gòu)M，狀態(tài)s和一個(gè)MvCTL狀態(tài)公式Φ，計(jì)算‖Φ‖(s)的值。其計(jì)算采用遞歸的方法。

給出模型檢測(cè)的算法[17]如下：

輸入：GPKSM和MvCTL公式Φ

輸出：s滿足公式φ的可能性，即‖Φ‖(s)

1：Procedure MvCTLCheck(Φ)

2：CaseΦ

3：rreturn (r)s∈S

4：areturn (L(s,a))s∈S

6：Φ1∧Φ2return (‖Φ1‖(s)∧‖Φ2‖(s))s∈S

7：Po(ΟΦ) returnP°Dψ°rp

9：Po(Φ1∪Φ2) return (DΦ°P)*°DΨ°rp

10：Po(◇Φ) returnP*°DΦ°rp

11：Po(□Φ) return Fixpoint((1)s∈S,fΦ)

End Case

End Procedure

3 模型檢測(cè)器的設(shè)計(jì)與實(shí)現(xiàn)

3.1 模型檢測(cè)器的架構(gòu)設(shè)計(jì)

模型檢測(cè)的基本運(yùn)行原理如圖1所示，主要分為三個(gè)部分：系統(tǒng)建模、性質(zhì)的形式化描述、模型檢測(cè)算法。所以模型檢測(cè)器的結(jié)構(gòu)設(shè)計(jì)也主要依據(jù)這三個(gè)部分來(lái)進(jìn)行。

圖1 模型檢測(cè)流程

模型檢測(cè)器分為三層。第一層為模型構(gòu)建層，主要完成對(duì)多值Kripke結(jié)構(gòu)中的數(shù)據(jù)進(jìn)行建模，用計(jì)算機(jī)中的數(shù)據(jù)結(jié)構(gòu)進(jìn)行存??；第二層為計(jì)算層，主要根據(jù)用戶輸入的性質(zhì)進(jìn)行計(jì)算；第三層為性質(zhì)驗(yàn)證層，主要對(duì)計(jì)算出的結(jié)果進(jìn)行驗(yàn)證，得出用戶輸入的性質(zhì)是否滿足系統(tǒng)的結(jié)果。模型檢測(cè)器的系統(tǒng)架構(gòu)如圖2所示。

圖2 模型檢測(cè)器架構(gòu)

3.2 格值轉(zhuǎn)換器設(shè)計(jì)

與經(jīng)典的模型檢測(cè)器的輸入不同時(shí)，由于采用了格值的建模方式，因此在驗(yàn)證之前，設(shè)計(jì)一個(gè)格值轉(zhuǎn)換器，主要方式是將格值映射到[0,1]區(qū)間上，例如三值邏輯，則將[T,M,F]映射為[0,0.5,1]的三值狀態(tài)進(jìn)行計(jì)算。

3.3 模型構(gòu)建層設(shè)計(jì)

需要保存Kripke結(jié)構(gòu)的節(jié)點(diǎn)信息以及傳遞信息，使用數(shù)據(jù)結(jié)構(gòu)中的圖[18]結(jié)構(gòu)。由于有向圖中有兩種存儲(chǔ)方式，一種是鄰接矩陣，一種是鄰接表，其相關(guān)的時(shí)間復(fù)雜度分別為Ο(n2)和Ο(E+V)(E為邊數(shù)，V為節(jié)點(diǎn)數(shù))，所以采用時(shí)間復(fù)雜度更低的鄰接表的方式進(jìn)行存儲(chǔ)。

根據(jù)用戶輸入的Kripke結(jié)構(gòu)，分別將節(jié)點(diǎn)和邊刻畫為Node類和Edge類，其中Node保存了節(jié)點(diǎn)的狀態(tài)信息，Edge類保存了傳遞信息。其實(shí)現(xiàn)為從用戶的輸入當(dāng)中生成所有的節(jié)點(diǎn)，然后依次遍歷每個(gè)節(jié)點(diǎn)信息，判斷節(jié)點(diǎn)與節(jié)點(diǎn)之間是否有邊，如有，則將邊的信息添加到鄰接表中，代碼如下：

/*******省略部分源碼*********/

public void addEdge(Node v,Node w){

if(hasEdge(v,w)){

Return;//如有邊，則返回

}

g.get(v.id).add(w);//g為list實(shí)例

}

3.4 計(jì)算層設(shè)計(jì)

這一層主要設(shè)計(jì)的問(wèn)題是模型檢測(cè)算法的輸入和計(jì)算函數(shù)的定義。將模型檢測(cè)算法封裝在一個(gè)函數(shù)當(dāng)中，接收用戶輸入的性質(zhì)，然后進(jìn)行判斷，判斷完成后，需要遍歷之前存儲(chǔ)的鄰接表，拿出狀態(tài)和傳遞的數(shù)據(jù)，最后調(diào)用計(jì)算函數(shù)進(jìn)行計(jì)算，將輸出的結(jié)果進(jìn)行保存。判斷函數(shù)的部分代碼如下：

//返回每一性質(zhì)計(jì)算所需要的公式類

publicFomule[] choiceFomule(String[] s){

//循環(huán)遍歷用戶的每一個(gè)輸入

for(int i=0;i

String s=s[i];

//match函數(shù)用于找到匹配的公式

Fomule[i] fomule=match(s);

}

returnfomule; //返回公式類

}

匹配公式之后，根據(jù)模型檢測(cè)算法進(jìn)行計(jì)算，需要定義圈乘“°”運(yùn)算，交運(yùn)算“∧”，并運(yùn)算“∨”的計(jì)算函數(shù)，圈乘函數(shù)代碼如下：

public double[n][n]calculateCircle(

double[n][n]a,double[n][n] b){

double[n][n] c=new double[n][n];

//遍歷a矩陣的行，遍歷b矩陣的列

for(int i=0;i

for(int j=0;j

if(a[i][j]

c[i][j]=a[i][j];

c[i][j]=b[j][i];

}

}

return c;//返回計(jì)算結(jié)果

}

對(duì)于并運(yùn)算函數(shù)和交運(yùn)算函數(shù)，由于和圈乘運(yùn)算類似，只是改變了取大和取小操作，這里省略了代碼。由于采用了雙層循環(huán)的遍歷，可以看出每個(gè)函數(shù)的時(shí)間復(fù)雜度為Ο(n2)。

3.5 驗(yàn)證層設(shè)計(jì)

這部分主要完成函數(shù)邏輯的調(diào)用，并計(jì)算出結(jié)果。由于在計(jì)算層封裝了各種算法公式，在驗(yàn)證層，需要拿出計(jì)算層給出的結(jié)果，加以判斷之后，輸出是或者否。將傳入計(jì)算層封裝的結(jié)果類ResultData，調(diào)用函數(shù)進(jìn)行判斷，返回一個(gè)boolean數(shù)組，最后遍歷這個(gè)數(shù)組可得到計(jì)算結(jié)果。

4 模型檢測(cè)器的驗(yàn)證

4.1 模型檢測(cè)器時(shí)間測(cè)試實(shí)驗(yàn)

對(duì)設(shè)計(jì)出來(lái)的模型檢測(cè)器做一個(gè)時(shí)間性能的測(cè)試。結(jié)果如表1所示，其中n表示狀態(tài)的個(gè)數(shù)，true表示正確完成了計(jì)算，false表示計(jì)算失敗，time表示運(yùn)行時(shí)間。

表1 運(yùn)行時(shí)間測(cè)試結(jié)果

模型檢測(cè)器在狀態(tài)數(shù)小于10 000的情況下，時(shí)間性能還不錯(cuò)，當(dāng)大于100 000時(shí)，由于時(shí)間復(fù)雜度是指數(shù)級(jí)增長(zhǎng)，時(shí)間性能上就差了一些。

4.2 恒溫器性質(zhì)驗(yàn)證實(shí)驗(yàn)

有一個(gè)三值恒溫器模型，如圖3所示。

接下來(lái)驗(yàn)證如下幾個(gè)性質(zhì)：

性質(zhì)1：系統(tǒng)是否可以從任何狀態(tài)轉(zhuǎn)移到IDLE1狀態(tài)；

性質(zhì)2：當(dāng)溫度低于某個(gè)值時(shí)加熱器是否可以啟動(dòng)；

性質(zhì)3：在任何情況下系統(tǒng)是否可以關(guān)閉；

性質(zhì)4：是否只有在空調(diào)關(guān)閉的狀態(tài)下才能加熱；

圖3 恒溫器模型

性質(zhì)5：當(dāng)溫度高于某個(gè)溫度時(shí)加熱器能否啟動(dòng)。

將這些性質(zhì)轉(zhuǎn)化為MvCTL公式后，輸入的結(jié)果如表2所示。

表2 性質(zhì)驗(yàn)證結(jié)果

通過(guò)表2可以得到一些結(jié)論，比如系統(tǒng)可以從狀態(tài)OFF轉(zhuǎn)移到狀態(tài)IDLE1的可能性為T,轉(zhuǎn)移到IDLE2的可能性為M，轉(zhuǎn)移到AC狀態(tài)的可能性為T。

5 結(jié)束語(yǔ)

根據(jù)基于多值可能性測(cè)度的多值可能性計(jì)算樹邏輯的模型檢測(cè)理論，設(shè)計(jì)能夠自動(dòng)化驗(yàn)證的多值模型檢測(cè)器MvChecker。根據(jù)模型檢測(cè)流程，設(shè)計(jì)了三層模型檢測(cè)器的框架，對(duì)每一層架構(gòu)進(jìn)行了詳細(xì)設(shè)計(jì)，并使用Java語(yǔ)言進(jìn)行了實(shí)現(xiàn)，用戶可以自己構(gòu)建系統(tǒng)和需要驗(yàn)證的性質(zhì)，輸入MvChecker進(jìn)行系統(tǒng)的驗(yàn)證。