丁如江, 李國(guó)強(qiáng)

(上海交通大學(xué) 軟件學(xué)院,上海 200240)

近年來,基于 Petri網(wǎng)的模型檢測(cè)技術(shù)已經(jīng)成功地應(yīng)用于并發(fā)程序的驗(yàn)證與分析[1-4]中.Petri網(wǎng)是一種適用于描述并發(fā)程序的模型,德國(guó)學(xué)者Sistla[5]首次提出了使用 Petri網(wǎng)來為程序建模的方法.具體來說,可以用Petri網(wǎng)模型中的位置(place)表示程序的狀態(tài),用模型中的遷移(transition)表示程序的執(zhí)行流,以及每個(gè)位置的令牌(token)數(shù)表示當(dāng)前有多少個(gè)進(jìn)程剛好運(yùn)行到該位置.

并發(fā)系統(tǒng)的安全性問題是指系統(tǒng)是否會(huì)有可能進(jìn)入某一錯(cuò)誤狀態(tài)(比如需保證進(jìn)程互斥的系統(tǒng)發(fā)生了多個(gè)進(jìn)程同時(shí)運(yùn)行到某一關(guān)鍵位置),規(guī)約到Petri網(wǎng)的可覆蓋性問題為:給定一個(gè)Petri網(wǎng)和一個(gè)狀態(tài)M(對(duì)應(yīng)到并發(fā)系統(tǒng)中的一個(gè)錯(cuò)誤狀態(tài)),是否會(huì)有一些由初始狀態(tài)M0可達(dá)的狀態(tài)M′覆蓋了M.如果存在可達(dá)狀態(tài)覆蓋錯(cuò)誤狀態(tài)M,就表明模型對(duì)應(yīng)的系統(tǒng)不是絕對(duì)安全的,系統(tǒng)在理論上會(huì)覆蓋這個(gè)錯(cuò)誤狀態(tài).現(xiàn)有的驗(yàn)證Petri網(wǎng)可覆蓋性的算法大致分為兩類:一類是基于Petri網(wǎng)狀態(tài)空間的遍歷,通過搜索Petri網(wǎng)的可達(dá)狀態(tài)空間來判斷是否覆蓋待驗(yàn)證狀態(tài)M.然而,由于Petri網(wǎng)的狀態(tài)空間規(guī)模與其位置遷移數(shù)是指數(shù)級(jí)別關(guān)系,所以這類算法在面對(duì)規(guī)模較大的Petri網(wǎng)時(shí)都顯得力不從心.比如BFC[4]、MIST、IIC[6]等工具都會(huì)有超時(shí)的問題存在.第2類是基于約束的,從Petri網(wǎng)的模型結(jié)構(gòu)以及待驗(yàn)證狀態(tài)中提取出約束條件,然后去求解這些約束來驗(yàn)證可覆蓋性.然而由于約束的表達(dá)能力有限,不可能完美地表達(dá)出Petri網(wǎng)的可達(dá)狀態(tài)空間,所以這些約束條件只能成為可覆蓋性問題的必要而非充分條件.因此,這類算法在理論上是不完備的,比如Petrinizer[7]工具只能驗(yàn)證那些安全的測(cè)試用例,對(duì)于不安全的測(cè)試用例則無法判定.

本文針對(duì)非交互式Petri網(wǎng)(communication-free Petri net),又被稱作基本并發(fā)進(jìn)程(basic parallel processes,簡(jiǎn)稱BPP),設(shè)計(jì)并實(shí)現(xiàn)了可以高效驗(yàn)證其可覆蓋性的工具(communication-free Petri net coverability verifier,簡(jiǎn)稱CFPCV).BPP在模型上的計(jì)算相對(duì)簡(jiǎn)單,其可覆蓋性問題是NP完備問題[8],同時(shí),它又能為一類并發(fā)程序建模并且進(jìn)行驗(yàn)證.我們采用基于約束的方法,從非交互式Petri網(wǎng)的模型結(jié)構(gòu)和待驗(yàn)證狀態(tài)中提取出約束,然后將這些約束交給Z3 SMT求解器求解.如果求解器得出無解,則說明不存在任何可達(dá)狀態(tài)覆蓋待驗(yàn)證狀態(tài),即待驗(yàn)證狀態(tài)不可覆蓋.而如果求解器有解(可能有多組解),并不能說明待驗(yàn)證狀態(tài)可覆蓋,因?yàn)榧s束條件的表達(dá)能力有限,滿足約束條件的狀態(tài)并不一定是該非交互式Petri網(wǎng)的可達(dá)狀態(tài),需要額外增加子網(wǎng)可標(biāo)記方法去驗(yàn)證該狀態(tài)是否可達(dá).如果驗(yàn)證通過,則說明待驗(yàn)證狀態(tài)可覆蓋.如果沒有通過,則需要迭代地去驗(yàn)證其他滿足約束條件的狀態(tài),直到最終得出結(jié)論,這樣就保證了該工具的算法在理論上是完備的,不存在無法判定的情況.同時(shí),只要對(duì)我們的約束條件稍加修改,CFPCV就可以很容易地驗(yàn)證BPP的可達(dá)性問題.

我們通過一個(gè)實(shí)例來說明基于約束驗(yàn)證 BPP可覆蓋性問題的方法,圖 1展現(xiàn)的是包含兩個(gè)進(jìn)程的并發(fā)程序及其對(duì)應(yīng)的非交互式Petri網(wǎng).

假定該并發(fā)程序需要維護(hù)一個(gè)寫鎖,即同一時(shí)刻最多只能有一個(gè)進(jìn)程可以獲取鎖來寫文件,對(duì)應(yīng)到非交互式Petri網(wǎng)為最多只能有1個(gè)進(jìn)程可以處在位置c,所以該非交互式Petri網(wǎng)必須滿足c≤1(即位置c內(nèi)的令牌數(shù)量不大于1)的性質(zhì),也就是說,滿足c≥2的狀態(tài)都是錯(cuò)誤狀態(tài).我們通過基于約束的方法來驗(yàn)證該非交互式Petri網(wǎng)是否會(huì)覆蓋滿足c=2的狀態(tài).首先根據(jù)BPP的模型要求,每個(gè)位置內(nèi)的令牌數(shù)以及每個(gè)遷移的觸發(fā)次數(shù)都必須大于等于 0,可以得到約束集{lock≥0,not lock≥0,c≥0,t1≥0,t2≥0,t3≥0,t4≥0,t5≥0,t6≥0}.然后根據(jù)位置和遷移的轉(zhuǎn)移關(guān)系得到約束集{lock=2+t5+t6–t1–t2,not lock=0+t1+t2–t3–t4,c=0+t3+t4–t5–t6}.最后加入待驗(yàn)證狀態(tài)的約束集{c≥2}.將這些約束集合并作為輸入交給Z3 SMT求解器求解,得出一個(gè)解{lock=0,not lock=0,c=2,t1=1,t2=1,t3=1,t4=1,t5=0,t6=0}.之后通過子網(wǎng)可標(biāo)記驗(yàn)證發(fā)現(xiàn)這組解確實(shí)是合法解,我們就可以判定該非交互式Petri網(wǎng)可以覆蓋滿足c=2的狀態(tài),從而說明對(duì)應(yīng)的并發(fā)程序是不安全的,可能會(huì)存在兩個(gè)進(jìn)程同時(shí)得到鎖一起寫文件的情況.

本文第1節(jié)介紹所用到的背景知識(shí),包括傳統(tǒng)Petri網(wǎng)、非交互式Petri網(wǎng)、可達(dá)性和可覆蓋性問題的數(shù)學(xué)定義,以及本文所使用到的Z3 SMT求解器介紹.第2節(jié)介紹驗(yàn)證非交互式Petri網(wǎng)可覆蓋性的安全性方法以及子網(wǎng)可標(biāo)記驗(yàn)證技術(shù).第3節(jié)介紹CFPCV的總體技術(shù)框架以及使用的算法細(xì)節(jié).第4節(jié)主要介紹實(shí)驗(yàn)及實(shí)驗(yàn)結(jié)果的分析.第5節(jié)介紹Petri網(wǎng)可覆蓋性研究的一些相關(guān)工作.第6節(jié)總結(jié)全文,并展望未來的工作.

1 預(yù)備知識(shí)

1.1 Petri網(wǎng)

Petri網(wǎng)可以用一個(gè)四元組N=(P,T,F,M0)來表示,其中,P是Petri網(wǎng)中所有位置的有限集合,T是Petri網(wǎng)中所有遷移的有限集合,F:(P×T)∪(T×F)→{0,1}稱為Petri網(wǎng)的流函數(shù),它表示位置和遷移之間的連接關(guān)系.而M0表示該 Petri網(wǎng)的初始狀態(tài).對(duì)于x∈P∪T,·x={y∈P∪T|F(y,x)=1},x·={y∈P∪T|F(x,y)=1}.·x記為x的前集或者輸入集,x·記為x的后集或者輸出集.Petri網(wǎng)的狀態(tài)M是一個(gè)從位置集合P映射到自然數(shù)的向量:P→?,該向量?jī)?nèi)的元素M(p)表示當(dāng)前狀態(tài)下位置p內(nèi)的令牌數(shù).

Petri網(wǎng)的可達(dá)性問題是指給定一個(gè)Petri網(wǎng)N=(P,T,F,M0)和一個(gè)狀態(tài)M,判斷M∈R(M0)是否成立,即判斷狀態(tài)M是否由M0到達(dá);可覆蓋性問題是指給定一個(gè)Petri網(wǎng)N=(P,T,F,M0)和一個(gè)狀態(tài)M,判斷是否存在一個(gè)狀態(tài)M′∈R(M0),滿足?p∈P,M′(p)≥M(p).如果存在,則稱該 Petri網(wǎng)覆蓋狀態(tài)M.

1.2 非交互式Petri網(wǎng)

非交互式Petri網(wǎng)是指滿足?t∈T,|·t|=1,即每個(gè)遷移的輸入位置數(shù)量為1的Petri網(wǎng)[8].它的可覆蓋性問題復(fù)雜度從Petri網(wǎng)的EXPSPACE完備降低到了NP完備.

1.3 SMT求解器

SAT問題被證明是第一個(gè)NP完備問題.作為SAT問題的擴(kuò)展,SMT問題[9]處理的對(duì)象是一階邏輯公式,相比于命題邏輯,增加了謂詞和量詞,很大程度上增強(qiáng)了SMT公式的表達(dá)能力.用以求解SMT問題的自動(dòng)化工具稱為SMT求解器.SMT求解技術(shù)在有界模型檢測(cè)、基于符號(hào)執(zhí)行的程序分析、線性規(guī)劃和調(diào)度、測(cè)試用例生成以及電路設(shè)計(jì)和驗(yàn)證等領(lǐng)域有非常廣泛的應(yīng)用.很多科研機(jī)構(gòu)以及公司都在致力研發(fā)正確率高、性能優(yōu)異的SMT求解器,并且已經(jīng)成功應(yīng)用到了具體的領(lǐng)域.目前流行的SMT求解器有:Barcelogic[10]、Beaver[11]、Yices[12]以及Z3[13]等.其中,由微軟公司主導(dǎo)開發(fā)的Z3 SMT求解器所支持的理論最多,性能也最好,因此本文使用了Z3 SMT求解器作為我們的求解引擎.

2 安全性方法與子網(wǎng)可標(biāo)記驗(yàn)證

本節(jié)主要介紹驗(yàn)證非交互式 Petri網(wǎng)可覆蓋性所用到的安全性方法以及子網(wǎng)可標(biāo)記驗(yàn)證技術(shù),在介紹安全性方法之前,我們首先介紹其核心——狀態(tài)方程的概念,最后介紹兩個(gè)加速剪枝的技巧.

2.1 狀態(tài)方程

對(duì)于一個(gè)給定的非交互式Petri網(wǎng)N=(P,T,F,M0),用一個(gè)大小為|P|的列向量M表示N的當(dāng)前狀態(tài),用一個(gè)大小為|T|的列向量X代表遷移序列σ中每個(gè)遷移觸發(fā)的次數(shù),那么狀態(tài)方程表示為

其中,C稱作關(guān)聯(lián)矩陣,它是一個(gè)|P|×|T|大小的矩陣,它的每一項(xiàng)的值按如下方法計(jì)算:

顯然,關(guān)聯(lián)矩陣記錄了該非交互式Petri網(wǎng)中每一個(gè)位置與遷移之間的連接關(guān)系.而X是遷移序列σ中每個(gè)遷移觸發(fā)的次數(shù).可以用Parikh映射(Parikh mapping)來表示它們之間的關(guān)系:

其中,ω(ti)代表遷移ti在遷移序列σ觸發(fā)的次數(shù).

比如對(duì)于圖3給定的非交互式Petri網(wǎng)和一個(gè)遷移序列σ=t1t2t1t3t2t1,就可以根據(jù)狀態(tài)方程計(jì)算出σ觸發(fā)后的新狀態(tài)M=[5,3,3,1,–1]T,其中,

2.2 安全性方法

安全性方法(safety method)是驗(yàn)證非交互式 Petri網(wǎng)可覆蓋性的基本方法,顧名思義,其目的就是為了驗(yàn)證非交互式Petri網(wǎng)對(duì)應(yīng)的并發(fā)系統(tǒng)是否安全.其基本思想是給定一個(gè)非交互式Petri網(wǎng)N和一個(gè)性質(zhì)φ,如果根據(jù)狀態(tài)方程M=M0+CX得出的所有狀態(tài)都不會(huì)違反?φ,則該非交互式Petri網(wǎng)一定滿足性質(zhì)φ.值得注意的是,如果狀態(tài)方程得出的某一個(gè)狀態(tài)M′滿足了?φ,并不能說明該非交互式 Petri網(wǎng)違反性質(zhì)φ.因?yàn)榍拔挠刑岬?狀態(tài)方程得出的狀態(tài)空間Set(M)是可達(dá)狀態(tài)空間R(M0)的超集,所以違反性質(zhì)φ的狀態(tài)M′不一定是該非交互式Petri網(wǎng)的可達(dá)狀態(tài).因此,安全性方法在理論上是不完備的,它只能在一個(gè)方向進(jìn)行驗(yàn)證,這也是安全性方法的局限所在.

本文只討論滿足如下條件的非交互式Petri網(wǎng).

1) 在任何合法的狀態(tài)下,每個(gè)位置的令牌數(shù)必須大于等于0.

2) 在任何合法的遷移序列中,每個(gè)遷移的觸發(fā)次數(shù)必須大于等于0.

結(jié)合狀態(tài)方程可以用如下約束條件表示[7]:

安全性方法用約束條件來表達(dá)就是將C(N)約束與待驗(yàn)證性質(zhì)φ的取反結(jié)合,表示為

約束(1)可以表示成多元一次等式和不等式的組合,而 SMT求解器可以很快地求解這些等式與不等式的組合.將約束(1)作為輸入交給SMT求解器求解,得出:

1) 無解,則說明狀態(tài)方程得出的狀態(tài)都不會(huì)違反性質(zhì)φ,即Set(M)|=φ,又因?yàn)镽(M0)?Set(M),所以R(M0)|=φ,繼而推出該非交互式Petri網(wǎng)N|=φ.也就說明對(duì)應(yīng)的并發(fā)系統(tǒng)是安全的.

2) 有解,則說明存在某狀態(tài)M′違反性質(zhì)φ,但由于Set(M)?R(M0),所以M′不一定是該非交互式Petri網(wǎng)N的可達(dá)狀態(tài),因此無法判定N是否滿足性質(zhì)φ,這也是安全性方法的局限所在.下一小節(jié)提出的子網(wǎng)可標(biāo)記驗(yàn)證方法,可以有效地判定候選狀態(tài)M′是否是N的可達(dá)狀態(tài),從而彌補(bǔ)了安全性方法的不足.

2.3 子網(wǎng)可標(biāo)記驗(yàn)證

前文介紹了驗(yàn)證非交互式Petri網(wǎng)可覆蓋性的安全性方法,雖然該算法借助于SMT求解器可以很高效地運(yùn)行,但是該算法在理論上卻不完備,只能驗(yàn)證非交互式Petri網(wǎng)N滿足性質(zhì)φ,卻無法得出N不滿足性質(zhì)φ的結(jié)論.原因是安全性方法依賴于狀態(tài)方程,對(duì)于狀態(tài)方程得出的候選狀態(tài)M′,我們無法判斷M′是否是N的可達(dá)狀態(tài).

而子網(wǎng)可標(biāo)記驗(yàn)證可以嚴(yán)謹(jǐn)?shù)嘏卸硞€(gè)狀態(tài)M′是否是非交互式Petri網(wǎng)的可達(dá)狀態(tài),從而可以彌補(bǔ)安全性方法的不足,在驗(yàn)證非交互式Petri網(wǎng)可覆蓋性時(shí)達(dá)到理論完備.

在介紹如何使用子網(wǎng)可標(biāo)記驗(yàn)證判定狀態(tài)M′是否為非交互式Petri網(wǎng)的可達(dá)狀態(tài)之前,需要引入如下的定義、引理與定理[8].

定義 1.給定一個(gè) Petri網(wǎng)N=(P,T,F)和一個(gè)遷移集合T的子集S,那么由S構(gòu)成的N的子網(wǎng)NS=(PS,S,FS).

定義2.給定一個(gè)Petri網(wǎng)N=(P,T,F,M0)和一個(gè)狀態(tài)M:

· 如果存在一個(gè)狀態(tài)M′,使得M′由M可達(dá),且M′(p)>0(其中,p∈P),則稱位置p由狀態(tài)M可標(biāo)記.

· 對(duì)于N的子網(wǎng)N′=(P′,T′,F′,M0′),如果N上的狀態(tài)M在N′上的投影為M′,且位置p(其中,p∈P′)由狀態(tài)M′可標(biāo)記,則稱位置p在N′上由M可標(biāo)記.

引理1.給定一個(gè)非交互式Petri網(wǎng)N和它的一個(gè)狀態(tài)M,一個(gè)位置p由狀態(tài)M可標(biāo)記當(dāng)且僅當(dāng)N中存在一條從p′到p的路徑,其中,p′滿足M(p′)>0.

引理1給出了一個(gè)在非交互式Petri網(wǎng)N上,快速判定位置p是否由狀態(tài)M可標(biāo)記的方法,即如果在M狀態(tài)下內(nèi)部令牌數(shù)大于0的某個(gè)位置p′,存在一條到位置p的路徑,那么就可以說明位置p在N上由M可標(biāo)記.也就是說,對(duì)于M狀態(tài)下內(nèi)部令牌數(shù)大于 0的位置,從這些位置經(jīng)過遷移可以到達(dá)的位置都是由狀態(tài)M可標(biāo)記的.

例如,針對(duì)圖3所示的Petri網(wǎng),給定向量X=[1,0,0]T,則子網(wǎng)NX如圖4所示,包含p1,p2,p3,p4這4個(gè)位置,t1一個(gè)遷移以及它們之間的流關(guān)系.在子網(wǎng)NX中,顯然,p1,p2,p3,p4都由狀態(tài)M0可標(biāo)記,因?yàn)镸0狀態(tài)下,p4內(nèi)的令牌數(shù)大于0,且p1,p2,p3都由p4可達(dá).

2) 子網(wǎng)NX內(nèi)的任一位置都能在NX上由M0可標(biāo)記.

定理 1給出了判定一個(gè)遷移觸發(fā)次數(shù)的向量X是否合法的充要條件,即在向量X的作用下,該非交互式Petri網(wǎng)的每個(gè)位置內(nèi)的令牌數(shù)必須大于等于0,而且子網(wǎng)NX內(nèi)的所有位置都必須由M0可標(biāo)記.結(jié)合定義2和引理 1,則定理 1的條件 2)可以表述為:NX內(nèi)的所有位置都必須由M0X可標(biāo)記,即?p∈PX,NX中都存在一條從p′(p′∈PX)到p的路徑,其中,p′滿足M0X(p′)＞0.如果X滿足定理1的兩個(gè)條件,則可以說明X合法,那么X作用下的狀態(tài)M就是可達(dá)狀態(tài),因?yàn)镸可以由M0通過σ到達(dá).這樣一來,我們就將判定非交互式Petri網(wǎng)上某個(gè)狀態(tài)是否可達(dá)規(guī)約到其對(duì)應(yīng)的遷移觸發(fā)次數(shù)向量X是否合法,使得問題變得更加具體,更加便于操作.

對(duì)于傳統(tǒng)的 Petri網(wǎng),我們很難判定某個(gè)狀態(tài)是否是可達(dá)狀態(tài).而對(duì)于非交互式 Petri網(wǎng),結(jié)合狀態(tài)方程與定理 1,可以有效地判定某個(gè)狀態(tài)是否可達(dá).我們可以通過狀態(tài)方程M′=M0+CX′求得M′對(duì)應(yīng)的解X′(可能有多個(gè)解),然后再去驗(yàn)證X′是否合法,如果合法,就可以得出M′可達(dá)的結(jié)論.而如果不合法,則可以迭代地去驗(yàn)證其余解,如果所有的解都不合法,就可以斷定M′不可達(dá).

在安全性方法中,任何非交互式Petri網(wǎng)N=(P,T,F,M0)都必須滿足C(N)約束,規(guī)定了在任何狀態(tài)下每個(gè)位置內(nèi)的令牌數(shù)都必須大于等于0,所以,定理1的第1個(gè)條件天然滿足.至于第2個(gè)條件,在安全性方法中,如果約束(1)有解(可能有多組解),即?M′∈Set(M),?φ(M′)成立.我們可以通過定理 1 來判定M′是否可達(dá),即判定其對(duì)應(yīng)的X′是否合法.這樣就可以嚴(yán)格地去驗(yàn)證非交互式Petri網(wǎng)是否覆蓋某個(gè)錯(cuò)誤狀態(tài),使得算法在理論上達(dá)到完備.

結(jié)合安全性方法與子網(wǎng)可標(biāo)記驗(yàn)證,驗(yàn)證非交互式Petri網(wǎng)可覆蓋性的方法可以表述如下.

以太網(wǎng)INTERNET模塊程序主要包括通過Xbee協(xié)調(diào)器對(duì)Xbee終端數(shù)據(jù)的接收與發(fā)送，以太網(wǎng)模塊W5100數(shù)據(jù)上傳與服務(wù)器控制命令的接收，其流程圖如圖4所示.以太網(wǎng)模塊程序首先配置網(wǎng)絡(luò)IP地址、DNS服務(wù)器等數(shù)據(jù)，再利用LEWEI50云平臺(tái)TCP通訊協(xié)議庫(kù)＜LeweiTcpClient.h＞實(shí)現(xiàn)數(shù)據(jù)上傳、遠(yuǎn)程開關(guān)的反向控制.

從非交互式Petri網(wǎng)N和待驗(yàn)證性質(zhì)φ中獲取約束條件C(P,T,F,M0)^?φ,作為SMT求解器的輸入進(jìn)行求解.

1) 無解,即約束條件不滿足,說明該非交互式Petri網(wǎng)的所有狀態(tài)都滿足性質(zhì)φ,N不會(huì)覆蓋滿足性質(zhì)?φ的錯(cuò)誤狀態(tài).

2) 有解,即?M′∈Set(M),?φ(M′)成立.我們需要去驗(yàn)證M′對(duì)應(yīng)的X′是否滿足定理 1 的第 2 個(gè)條件.

a) 若滿足,說明?φ會(huì)被一個(gè)可達(dá)狀態(tài)滿足,表明N不滿足性質(zhì)φ,N會(huì)覆蓋滿足性質(zhì)?φ的錯(cuò)誤狀態(tài).

b) 若不滿足,說明滿足?φ的狀態(tài)M′不可達(dá).由于滿足約束C(P,T,F,M0)^?φ的狀態(tài)可能有多個(gè),所以需要加上新的約束條件剔除狀態(tài)M′,繼續(xù)交給SMT求解器求解,進(jìn)行下一次迭代(注:由于約束(1)中等式的數(shù)量可能少于變量的個(gè)數(shù),且約束中存在不等式,所以約束(1)的解的數(shù)量可能是無限的,而且可能存在需要無數(shù)次迭代的極端情況.不過,從之后的測(cè)試發(fā)現(xiàn),多次迭代的情況非常少.當(dāng)然,約束(1)解的數(shù)量并不等于迭代的次數(shù),因?yàn)槊看蔚⒉灰欢ㄖ慌懦粋€(gè)解,也可能是一組甚至無數(shù)解,可以參考第 3.3節(jié)中的實(shí)例,而排除解的數(shù)量在不同的模型中也互不相同,所以約束(1)解的數(shù)量和迭代次數(shù)之間的關(guān)系并不能用確切的表達(dá)式來表達(dá).甚至可能存在約束(1)解的數(shù)量無限,但是只需要幾次迭代即可成功驗(yàn)證的情況).

2.4 剪枝技巧

因?yàn)閷?duì)于 SMT求解器的每組解,我們都需要驗(yàn)證其是否符合定理 1的條件 2),為了減少算法的迭代次數(shù),我們可以增加兩種剪枝加速的方法.

1) 在給定的非交互Petri網(wǎng)N=(P,T,F,M0)中,對(duì)于那些滿足M0(p)>0的位置,它們的輸出遷移必須至少有一個(gè)觸發(fā)次數(shù)大于0.約束化為Constraints1.

因?yàn)槲覀円?yàn)證每組解是否符合定理1的條件2),也就是子網(wǎng)內(nèi)的每個(gè)位置都要由M0可標(biāo)記.由引理1可知,該子網(wǎng)內(nèi)至少有一個(gè)位置p滿足M0(p)>0.因此,如果Constraint1無法滿足,也就是說,滿足M0(p)>0的位置p根本沒有路徑“出去”,則子網(wǎng)內(nèi)的其他位置p′都無法由M0可標(biāo)記.

2) 在給定的非交互Petri網(wǎng)N=(P,T,F,M0)中,如果存在這樣的位置,InitPlace集合中的任意一個(gè)位置都不存在一條到它的路徑,那么它的輸入和輸出遷移發(fā)生的次數(shù)都為0.約束化為Constraints2.

因?yàn)閷?duì)于這些無法從InitTransition中的位置到達(dá)的位置,它們?cè)谌魏螤顟B(tài)子網(wǎng)上都是無法由M0可標(biāo)記的,如果它們的輸入或者輸出遷移發(fā)生的次數(shù)大于 0,那么子網(wǎng)就必須將這些位置包含進(jìn)去,那么該子網(wǎng)就不可能滿足定理1的條件2).

使用上述兩種剪枝技巧,可以有效地減少算法的迭代次數(shù),使得驗(yàn)證更加高效、實(shí)用.

3 CFPCV工具技術(shù)框架

我們采用基于約束的方法,實(shí)現(xiàn)了可以高效驗(yàn)證非交互式Petri網(wǎng)可覆蓋性的工具CFPCV,它在安全性方法的基礎(chǔ)上,加上子網(wǎng)可標(biāo)記驗(yàn)證,從而使得該算法在理論上完備.本節(jié)主要介紹 CFPCV工具的技術(shù)架構(gòu)以及使用到的具體算法.

3.1 技術(shù)架構(gòu)

本文的技術(shù)方案如圖5所示.主要分為約束提取、約束求解、候選解驗(yàn)證、增加約束進(jìn)行迭代這4個(gè)部分.具體內(nèi)容如下.

1) 首先根據(jù)給定的非交互Petri網(wǎng)模型N=(P,T,F,M0)得到一些模型的基本約束,例如每個(gè)位置內(nèi)的令牌數(shù)必須大于等于 0,每個(gè)遷移發(fā)生的次數(shù)必須大于等于 0,再根據(jù)需要驗(yàn)證的狀態(tài)M得到狀態(tài)約束,例如待驗(yàn)證性質(zhì)為p1=1&p2=1,則約束p1≥1&p2≥1可以覆蓋滿足此性質(zhì)的狀態(tài).

2) 將步驟1)得到的約束條件和剪枝技巧合并為約束文件,作為輸入交給SMT求解器求解.

3) 如果無解,則表明不存在滿足這些約束條件的狀態(tài),也就是說,N不能覆蓋狀態(tài)M′;如果有解并不能代表N覆蓋狀態(tài)M,只能代表M′滿足這些約束條件,還必須驗(yàn)證M′由M0可達(dá),即需要將狀態(tài)M′從狀態(tài)方程的狀態(tài)空間壓縮到該非交互式Petri網(wǎng)的可達(dá)狀態(tài)空間內(nèi).

4) 如果驗(yàn)證出M′狀態(tài)確實(shí)由M0可達(dá),則可以表明N覆蓋M;如果不可達(dá),說明SMT求解器求出的這組解(基于約束條件可能有很多組解,求解器每次只給出一組解)不滿足要求.需要將狀態(tài)M′代表的這一類狀態(tài)剔除,即生成新的約束加入到約束文件中,重復(fù)步驟3)和步驟4),直到程序得到解退出為止.

3.2 算法實(shí)現(xiàn)

CFPCV工具使用到的核心算法偽代碼如下.

關(guān)于算法的邏輯,前文已經(jīng)解釋清楚,主要分為約束提取、約束求解、候選解驗(yàn)證、增加約束進(jìn)行迭代這4個(gè)部分,這里不再贅述.其中,第 8行的代碼表示提取新約束來剔除子網(wǎng)SN所代表的一系列解.比如,T={t1,t2,t3,t4},X={1,0,3,1}.那么,SN就是根據(jù)t1,t3,t4這3個(gè)遷移構(gòu)成的子網(wǎng),如果子網(wǎng)SN不滿足定理1的條件2),則在下一次迭代中,必須增加約束將SN所代表的一系列解剔除,即新約束δ為not(t1>0 &t2=0 &t3>0 &t4>0).

3.3 算法求解示例

我們可以通過一個(gè)實(shí)例再進(jìn)一步更加直觀、清晰地認(rèn)識(shí)這一算法,對(duì)于圖8給定的非交互式Petri網(wǎng)和帶驗(yàn)證性質(zhì)φ(p1+p3<3),安全性約束C(P,T,F,M0)^?φ為

p1,p2,p3,p4≥0

t1,t2,t3,t4,t5≥0

p1=0+t5

p2=1+t3+t4

p3=0+t3+t4+t5

p4=0+t1+t2+t3+t4–t5

p1+p3≥3

兩種剪枝約束Constraint1(2)和Constraint2(3).

t2>0

將上述約束作為輸入交給SMT求解器求解,有解,解ModelA1為

p1=0,p2=3,p3=3,p4=4

t1=0,t2=1,t3=0,t4=3,t5=0

所以X1=(0,1,0,3,0),構(gòu)成的子網(wǎng)NX1如圖6所示.

顯然,該子網(wǎng)中只有p2,p4由M0可標(biāo)記,因此需要增加新約束δnot(t1=0 &t2>0 &t3=0 &t4>0 &t5=0),剔除該子網(wǎng)進(jìn)行下一次迭代,下一次迭代的約束即為

p1,p2,p3,p4≥0

t1,t2,t3,t4,t5≥0

p1=0+t5

p2=1+t3+t4

p3=0+t3+t4+t5

p4=0+t1+t2+t3+t4–t5

p1+p3≥3

t2>0

not(t1=0 &t2>0 &t3=0 &t4>0 &t5=0)

將新的約束文件作為輸入交給SMT求解器求解,依然有解,解ModelA2為

p1=1

p2,p2,p3=3

t1,t2,t3,t4,t5=1

所以X2=(1,1,1,1,1),而由NX2構(gòu)成的子網(wǎng)如圖7所示.

4 實(shí)驗(yàn)及結(jié)果分析

由于現(xiàn)有的驗(yàn)證可覆蓋性問題的工具都是針對(duì)傳統(tǒng) Petri網(wǎng)的,它們所使用到的標(biāo)準(zhǔn)測(cè)試集也都是傳統(tǒng)Petri網(wǎng),所以這些測(cè)試集對(duì)于CFPCV工具的測(cè)試不再適用.因此,針對(duì)非交互式Petri網(wǎng),我們隨機(jī)生成了3組非交互式Petri網(wǎng)的測(cè)試用例,它們的位置和遷移數(shù)規(guī)模分別是1～10、1～100、1～1000.我們主要從成功率、迭代次數(shù)、性能比這3個(gè)方面對(duì)CFPCV進(jìn)行了評(píng)測(cè).我們主要與Petrinizer、MIST這兩個(gè)工具進(jìn)行了比較,Petrinizer工具是通過提取約束并求解的方法來驗(yàn)證傳統(tǒng) Petri網(wǎng)的可覆蓋性問題,與 CFPCV一樣,它也是采用安全性方法來獲得約束.不過,正如前文所述,安全性方法在理論上是不完備的,其只能驗(yàn)證那些覆蓋的用例,對(duì)于不覆蓋的用例則無能為力.但從文獻(xiàn)[7]中的實(shí)驗(yàn)結(jié)果來看,Petrinizer在應(yīng)對(duì)一些特定的測(cè)試集時(shí)仍然有不錯(cuò)的成功率.而 MIST工具是采用狀態(tài)空間探索的方法,其內(nèi)部集成了多種驗(yàn)證算法,包括從待驗(yàn)證狀態(tài)反向探索狀態(tài)空間的backward[14]算法,以及先對(duì)原Petri網(wǎng)模型進(jìn)行抽象精化(abstraction refinement)來縮小模型規(guī)模,然后再結(jié)合前驅(qū)和反向探索狀態(tài)空間來進(jìn)行驗(yàn)證的 ic4pn[15]算法、tsi[15]算法和 eec[16]算法.盡管增加了抽象精化的過程來縮小模型的規(guī)模,但是對(duì)于隨機(jī)模型這個(gè)過程的效果甚微,依然會(huì)有狀態(tài)爆炸(state explosion)的問題存在.

4.1 成功率

我們將隨機(jī)生成的3組測(cè)試用例作為輸入交給CFPCV、Petrinizer、MIST工具求解,后兩種工具都是驗(yàn)證傳統(tǒng)Petri網(wǎng)可覆蓋性的工具,所以它們肯定也可以驗(yàn)證非交互式Petri網(wǎng)的可覆蓋性問題.我們分別比較了這3種工具在每組測(cè)試用例下的成功率,見表1～表3(注:Positive表示滿足性質(zhì)φ,Negative表示不滿足,Timeout表示超時(shí),Don’t know表示無法判定,Success rate表示成功率).

從3張表可以發(fā)現(xiàn),Petrinizer工具的成功率最低,因?yàn)镻etrinizer使用到的方法也是安全性方法,但因其針對(duì)傳統(tǒng)Petri網(wǎng),并沒有子網(wǎng)可標(biāo)記驗(yàn)證來保證候選解是正確解,所以該工具使用到的算法在理論上不完備,可能存在其無法判定的情況,所以對(duì)于隨機(jī)生成的測(cè)試用例,有大量的測(cè)試用例其無法判定,因此成功率在 3種工具中最低,在第3組測(cè)試用例上只有4.6%的成功率.而MIST工具是基于Petri網(wǎng)可達(dá)狀態(tài)空間的搜索,由于Petri網(wǎng)的可達(dá)狀態(tài)空間可能很大,所以該工具經(jīng)常發(fā)生超時(shí)情況,對(duì)于規(guī)模較大的輸入,超時(shí)情況更加嚴(yán)重.所以,對(duì)于隨機(jī)生成的測(cè)試用例,MIST工具超時(shí)最多,而且隨著測(cè)試用例規(guī)模的擴(kuò)大,其超時(shí)情況變得非常嚴(yán)重,成功率直接從100%下降到了46.9%.顯然,CFPCV工具的成功率最為優(yōu)異,對(duì)于3組測(cè)試用例成功率都在99%以上.

Table 1 Success rate of the 3 tools in test cases which scales of place and transition are between 1 to 10表1 測(cè)試用例位置遷移數(shù)規(guī)模1～10之間3種工具的成功率

Table 2 Success rate of the 3 tools in test cases which scales of place and transition are between 1 to 100表2 測(cè)試用例位置遷移數(shù)規(guī)模1～100之間3種工具的成功率

Table 3 Success rate of the 3 tools in test cases which scales of place and transition are between 1 to 1000表3 測(cè)試用例位置遷移數(shù)規(guī)模1～1000之間3種工具的成功率

4.2 迭代次數(shù)

因?yàn)?CFPCV 使用到的算法是基于迭代的,需要在每次迭代中驗(yàn)證候選解是否是正確解,如果不是,則需要增加約束繼續(xù)迭代求解,所以算法的迭代次數(shù)直接決定了算法的運(yùn)行效率.如果迭代次數(shù)過多,就可能發(fā)生超時(shí)的情況.我們記錄了每組測(cè)試用例算法的迭代次數(shù),見表4.

由表 4可以發(fā)現(xiàn),對(duì)于絕大多數(shù)(2587+397)測(cè)試用例,只需要 1～2次迭代即可得解,只有極個(gè)別的測(cè)試用例需要10次以上的迭代(12次2個(gè),16次1個(gè),超時(shí)10個(gè)).因?yàn)橹恍枰苌俚牡螖?shù)即可得解,所以CFPCV工具的運(yùn)行效率理應(yīng)很高.

Table 4 Iteration time of CFPCV表4 CFPCV運(yùn)行迭代次數(shù)

4.3 性能比

因?yàn)镃FPCV和Petrinizer都用到了安全性方法,且Petrinizer的性能也非常高,只不過其成功率較低,所以我們比較了3組測(cè)試用例下這兩種工具的性能(未比較MIST是因?yàn)镸IST超時(shí)情況嚴(yán)重,所以其性能自然較低),性能比如圖9～圖11所示,單位為s.

由圖9～圖11可知,Petrinizer和CFPCV性能相當(dāng),大部分測(cè)試用例兩種工具在20s內(nèi)得解.圖中箭頭標(biāo)注的點(diǎn)分為兩類,一類是CFPCV需要的較多的迭代才可得解,因此這些點(diǎn)代表的測(cè)試用例CFPCV運(yùn)行較慢.另一類是兩種工具都超時(shí)(圖11右上角的8個(gè)點(diǎn)),原因是因?yàn)镾MT求解器求解約束超時(shí),這種情況是合理的,因?yàn)橛行┘s束求解問題(比如SAT問題)就是NP完備問題,可能存在一些測(cè)試用例SMT求解器根本無法求解,因此兩種工具都發(fā)生了超時(shí)的情況.因?yàn)镻etrinizer沒有驗(yàn)證候選解的迭代過程,所以Petrinizer的性能理應(yīng)比CFPCV要好.但是由第 4.2節(jié)迭代次數(shù)的記錄來看,對(duì)于絕大多數(shù)測(cè)試用例,CFPCV只需要一兩次迭代即可得解,因此CFPCV的性能和Petrinizerx相差無幾.考慮到第4.1節(jié)提到的CFPCV極高的成功率,這樣的性能是非常令人欣慰的.

5 相關(guān)工作

Petri網(wǎng)的可覆蓋性問題雖然已被證明是EXPSPACE完備問題[17,18],BPP的可達(dá)性以及可覆蓋性問題也都被證明是NP完備問題[3],但是近年來學(xué)術(shù)界依然提出了很多解決該問題的算法,它們可以大致分為兩類:第1類就是基于狀態(tài)空間的探索.由Karp和Miller(簡(jiǎn)稱KM)提出的Karp and Miller procedure[17]是第一個(gè)可以驗(yàn)證Petri網(wǎng)可覆蓋性的完備算法,它的主要思想是從Petri網(wǎng)的初始狀態(tài)前驅(qū)探索(forward exploration)狀態(tài)空間,不斷加入可以覆蓋前一狀態(tài)的新狀態(tài)來構(gòu)造 Petri網(wǎng)的覆蓋樹,然后判斷待驗(yàn)證狀態(tài)是否在該覆蓋樹上來進(jìn)行驗(yàn)證.但是,由于 Petri網(wǎng)的可達(dá)狀態(tài)可以無限制地增長(zhǎng),導(dǎo)致覆蓋樹的規(guī)模可能非常之大,所以這個(gè)構(gòu)造過程通常比較低效,它具有非原始遞歸最壞情況的復(fù)雜度.這項(xiàng)技術(shù)已在 TINA-KM[19]工具上實(shí)現(xiàn),可想而知,該工具在處理狀態(tài)空間較大的模型時(shí)效率很低.另外,這項(xiàng)技術(shù)的一種優(yōu)化方法就是構(gòu)造 Petri網(wǎng)的最小覆蓋集(minimal coverability sets)[20]而非覆蓋樹,最小覆蓋集已被證明是存在且有限的[21],而且其規(guī)模要遠(yuǎn)小于覆蓋樹的規(guī)模,所以其構(gòu)造效率有了較大的提升,這項(xiàng)技術(shù)已在 Pep[22]工具上實(shí)現(xiàn).另外,還有反向探索(backward exploration)[23]狀態(tài)空間的算法,就是從待驗(yàn)證狀態(tài)反向探索狀態(tài)空間,直到到達(dá)初始狀態(tài)為止,這項(xiàng)技術(shù)已在工具 IST-BC和PETR-BC[24]上實(shí)現(xiàn),不過,反向探索和前驅(qū)探索本質(zhì)上沒有太大的區(qū)別,所以算法效率并沒有顯著的提升.當(dāng)然,還有將前驅(qū)探索和反向探索結(jié)合[25,26]的算法,分別從初始狀態(tài)前驅(qū)探索狀態(tài)空間和從待驗(yàn)證狀態(tài)反向探索狀態(tài)空間,直到兩條探索路徑觸碰為止,這項(xiàng)技術(shù)已在工具BFC上實(shí)現(xiàn),性能得到了較大的提升.文獻(xiàn)[16]中提出的‘Expand, Enlarge and Check’方法通過并發(fā)地構(gòu)造兩個(gè)Petri網(wǎng)的近似序列來驗(yàn)證可覆蓋性,第1個(gè)序列是系統(tǒng)的向下近似,它可以用來判定覆蓋的實(shí)例,另外一個(gè)序列是系統(tǒng)的向上近似,用來判定那些不覆蓋的實(shí)例.這項(xiàng)技術(shù)已在工具 MIST上實(shí)現(xiàn).MIST內(nèi)部集成了多種算法,不過,它們的思路大體一致,都是先對(duì)原模型進(jìn)行一層抽象來縮小模型的規(guī)模,然后對(duì)抽象后的模型通過前驅(qū)探索和反向探索結(jié)合的方法來加以驗(yàn)證.另外一類是基于約束的方法.其主要思想與本文的算法類似,都是用約束條件來表達(dá)Petri網(wǎng)的性質(zhì),通過求解約束來驗(yàn)證可覆蓋性.然而,由于約束的表達(dá)能力有限,不可能準(zhǔn)確表述出 Petri網(wǎng)的可達(dá)狀態(tài)空間,所以這些約束條件只能成為可覆蓋性問題的必要條件而非充分條件.因此這類算法在理論上是不完備的,比如 Petrinizer[7]工具,它是通過安全性方法來提取約束并求解來進(jìn)行驗(yàn)證,不過,由于安全性方法在理論上不完備,所以它只能驗(yàn)證那些不覆蓋的測(cè)試用例,對(duì)于覆蓋的測(cè)試用例則無法驗(yàn)證.

除此之外,并發(fā)程序的性質(zhì)也可以通過基于 Petri網(wǎng)的模型檢測(cè)技術(shù)來分析,使用 TCTL(時(shí)間計(jì)算樹邏輯)[27]來描述待驗(yàn)證性質(zhì),通過檢測(cè) Petri網(wǎng)的遷移發(fā)生序列來驗(yàn)證模型是否滿足這些性質(zhì).其具體思路是先構(gòu)造包含待驗(yàn)證性質(zhì)取反語義序列的Büchi自動(dòng)機(jī),然后再計(jì)算Petri網(wǎng)可達(dá)圖和自動(dòng)機(jī)的乘積圖.若將乘積圖看成一個(gè)有向圖,則模型檢測(cè)的問題等價(jià)于檢測(cè)乘積圖中是否包含一個(gè)從初始狀態(tài)可達(dá)的最大強(qiáng)連通分量,且在該強(qiáng)連通分量中包含了一個(gè)接受狀態(tài).對(duì)于安全性一類的性質(zhì)來說,等價(jià)于檢測(cè)乘積圖中是否存在一條從初始節(jié)點(diǎn)到接受節(jié)點(diǎn)的路徑.對(duì)于活性一類的性質(zhì)來說,等價(jià)于檢測(cè)乘積圖中是否存在由初始節(jié)點(diǎn)可達(dá)的包含接受節(jié)點(diǎn)的環(huán).但是,基于 Petri網(wǎng)的模型檢測(cè)技術(shù)也會(huì)受到狀態(tài)爆炸問題的困擾,因?yàn)?Petri網(wǎng)模型的狀態(tài)空間通常非常之大,甚至無界,所以 Petri網(wǎng)的模型檢測(cè)問題難度非常之大,其上的很多邏輯算子都不存在多項(xiàng)式時(shí)間算法.比如EG/AF(即我們通常所說的活性)邏輯在Petri網(wǎng)和BPP上都是不可判定的,EF邏輯在Petri網(wǎng)同樣不可判定,在BPP上雖然可判定,但也擁有PSPACE完備的復(fù)雜度[28].所以,傳統(tǒng)的基于Petri網(wǎng)的模型檢測(cè)技術(shù)在驗(yàn)證并發(fā)程序的性質(zhì)時(shí)存在較大的局限性.

6 總結(jié)及未來的工作

本文設(shè)計(jì)并實(shí)現(xiàn)了可以高效驗(yàn)證非交互式Petri網(wǎng)可覆蓋性的工具CFPCV,它在驗(yàn)證傳統(tǒng)Petri網(wǎng)可覆蓋性使用到的安全性方法的基礎(chǔ)上,增加了只對(duì)非交互式Petri網(wǎng)適用的子網(wǎng)可標(biāo)記驗(yàn)證,從而保證了其解的正確性,并且通過實(shí)驗(yàn)驗(yàn)證了該工具具有較高的成功率以及不錯(cuò)的性能.

由于業(yè)界缺乏針對(duì)非交互 Petri網(wǎng)可覆蓋性驗(yàn)證的標(biāo)準(zhǔn)測(cè)試集,所以本文測(cè)試所使用測(cè)試集都是隨機(jī)產(chǎn)生的.未來會(huì)使用數(shù)量更多以及質(zhì)量更高的測(cè)試集進(jìn)行測(cè)試,以驗(yàn)證 CFPCV的表現(xiàn)是否依然優(yōu)秀.另外,其實(shí)除了本文所提的剪枝方法以外,還有一種叫作阱(trap)約束[29]的技巧可以進(jìn)行加速,不過我們通過測(cè)試發(fā)現(xiàn),阱約束的表現(xiàn)卻不盡人意,可能和我們測(cè)試集的隨機(jī)性有關(guān).未來業(yè)界若有質(zhì)量較高的測(cè)試集公開,我們會(huì)在算法上增加阱約束進(jìn)行測(cè)試,如果性能得到提升,則將加以改進(jìn).

未來,我們也會(huì)在BPP上做模型檢測(cè),雖然第5節(jié)提到BPP上的模型檢測(cè)問題難度很大,但是我們?nèi)绻鲇薪缒Ｐ蜋z測(cè),比如將某個(gè)性質(zhì)在無限的轉(zhuǎn)移序列上都要成立限定為在k(k為大于0的自然數(shù))步轉(zhuǎn)移內(nèi)成立,同時(shí)也保證這樣的性質(zhì)具有一定的實(shí)際意義,那么問題的復(fù)雜度將大幅下降.同樣通過提取約束,使用 SMT求解器求解約束的方法,BPP上的有界模型檢測(cè)問題可能會(huì)有很高效的解決方案.