左貴征,趙嶺忠

基于ASP及穩(wěn)定失敗語義的CSP模型檢測

左貴征,趙嶺忠

(桂林電子科技大學(xué)計算機科學(xué)與工程學(xué)院,廣西桂林 541004)

針對現(xiàn)有模型檢測工具對活性描述不足、模型轉(zhuǎn)換復(fù)雜,提出一種基于ASP及穩(wěn)定失敗語義的CSP模型檢測方法。該方法采用時態(tài)邏輯LTL刻畫性質(zhì),將進程的穩(wěn)定失敗模型和LTL公式轉(zhuǎn)化為ASP,利用ASP求解器驗證性質(zhì),實現(xiàn)一次運行驗證多條性質(zhì)。實驗結(jié)果表明,該方法既擴大了基于穩(wěn)定失敗模型的活性驗證范圍,也避免了不同模型之間的轉(zhuǎn)換。

通信順序進程;線性時態(tài)邏輯;穩(wěn)定失敗語義;回答集程序設(shè)計

CSP[1]是由Hoare提出的一種代數(shù)語言,主要用于對并發(fā)系統(tǒng)進行刻畫和驗證。隨著CSP在并發(fā)系統(tǒng)、通信協(xié)議等領(lǐng)域的廣泛應(yīng)用,CSP進程的形式化驗證成為一個重要的研究課題。目前,CSP驗證主要采用定理證明和模型檢測,以操作語義和指稱語義作為理論基礎(chǔ)。

跡模型和穩(wěn)定失敗模型是2種典型的指稱語義模型,跡模型描述了進程可執(zhí)行的行為序列,可用于確定性進程的性質(zhì)驗證。然而,跡模型存在以下不足[2]:1)對所有進程統(tǒng)一采用行為序列描述,不能區(qū)分外部選擇和內(nèi)部選擇,不能完全描述進程行為。如進程M1=(a→stop),M2=(b→stop),則進程M1| M2與進程的跡集均為{〈a〉,〈b〉}。2)不能驗證不同環(huán)境下非確定性進程的相關(guān)性質(zhì)。

基于此,Roscoe提出了CSP進程的穩(wěn)定失敗模型[2],該模型擴充了拒絕集描述進程拒絕執(zhí)行的事件,實現(xiàn)了無發(fā)散進程的活性驗證。文獻[3]給出了一種用于CSP進程精化驗證的交互式定理證明器CSP-mrover,在穩(wěn)定失敗模型中,可通過完備度量空間和完全偏序理論驗證無邊界非確定性的無限狀態(tài)系統(tǒng)性質(zhì)。文獻[4]針對嵌入CSP跡模型的MVS只能驗證進程安全性的問題,提出一種將MVS與CSP穩(wěn)定失敗模型相結(jié)合的方法,實現(xiàn)了進程確定性和無死鎖的驗證。

上述2種方法均采用定理證明,但定理證明的自動化程度不高,不能自動執(zhí)行,且需要用戶有較深的數(shù)學(xué)造詣,從而限制了它們的應(yīng)用。主流的模型檢測工具FDR通過操作語義將進程轉(zhuǎn)化為遷移系統(tǒng),通過對應(yīng)的指稱語義實現(xiàn)系統(tǒng)性質(zhì)的驗證。然而,由于涉及到多個模型之間的轉(zhuǎn)換,增加了復(fù)雜度。文獻[5-7]證明了FDR只能驗證部分活性謂詞,一些重要的活性謂詞可用LTL公式表述,但無法用FDR驗證。

為了解決以上問題,提出基于ASP[8]及穩(wěn)定失敗語義的模型檢測,采用LTL[9]公式進行性質(zhì)描述,擴大了基于穩(wěn)定失敗語義所驗證性質(zhì)的范圍。此外,也避免進程不同模型之間的轉(zhuǎn)換,降低了計算復(fù)雜度。另外,利用ASP求解器可同時驗證多條性質(zhì)。

1 ASP簡介

ASP是具有聲明特征的知識表示和推理的邏輯設(shè)計語言,它的基礎(chǔ)是回答集語義,可方便地用于非單調(diào)知識的表示和推理,且具有很強的聲明性,可對問題自動求解,具有強大的知識表示能力。每個程序是一組規(guī)則集合,且規(guī)則滿足:

a1∨…∨ak←ak+1,…,am,not am+1,…,not an。其中ai為謂詞。k＞1的規(guī)則稱為析取規(guī)則,{a1,a2,…,ak}為析取;k=1的規(guī)則稱為標(biāo)準規(guī)則;k=0的規(guī)則稱為完整約束;k=n的規(guī)則稱為事實。

通過ASP解決問題時,利用ASP程序?qū)栴}進行描述,使用ASP求解器DLV對描述的ASP程序求解,得到的回答集即為相應(yīng)問題的解。

2 模型檢測框架

基于ASP及穩(wěn)定失敗語義的并發(fā)系統(tǒng)CSP模型檢測用CSP描述系統(tǒng)的行為,用通用的LTL描述系統(tǒng)性質(zhì),然后,將CSP和LTL分別轉(zhuǎn)化為ASP描述和規(guī)則,將描述和規(guī)則集輸入到求解器中,得到對應(yīng)的回答集,這樣“給定系統(tǒng)中,性質(zhì)能否成立”就改變?yōu)椤芭袛嗷卮鸺惺欠翊嬖谛再|(zhì)標(biāo)記”。ASP下基于穩(wěn)定失敗語義的CSP驗證框架如圖1所示。

圖1 ASP下基于穩(wěn)定失敗語義的CSP模型檢測框架Fig.1 CSP verification framework based on ASP and stable failure semantics

將該框架劃分為兩部分設(shè)計與實現(xiàn):

1)CSP并發(fā)系統(tǒng)及其穩(wěn)定失敗模型的ASP描述和對應(yīng)規(guī)則。定義謂詞實現(xiàn)進程的描述,根據(jù)這些謂詞定義對應(yīng)穩(wěn)定失敗模型(包括進程的跡和拒絕集)的生成規(guī)則。其中,進程包括基本進程和并發(fā)組合,尤其是內(nèi)部選擇和外部選擇的區(qū)分尤為重要。

2)LTL公式到ASP規(guī)則的轉(zhuǎn)換。穩(wěn)定失敗模型可描述事件發(fā)生的必須性和可能性,LTL中存在公式a描述事件a一定發(fā)生。因此,增加公式available a描述事件a可發(fā)生,但不是必須發(fā)生。最后,給出LTL公式穩(wěn)定失敗語義下的ASP描述。

3 CSP穩(wěn)定失敗模型的ASP描述

CSP并發(fā)系統(tǒng)由進程通過不同的算子組合而成,針對不同算子,分別定義對應(yīng)的謂詞描述及規(guī)則,從而通過組合實現(xiàn)并發(fā)系統(tǒng)的ASP描述及穩(wěn)定失敗模型的生成。

進程的穩(wěn)定失敗模型一般包括進程的跡(可執(zhí)行行為序列)和拒絕集(可拒絕的事件集合),因此,分別針對跡和拒絕集構(gòu)造不同的謂詞及規(guī)則,從而實現(xiàn)穩(wěn)定失敗模型的描述。

文獻[10]已定義了所需的大部分符號謂詞,將其擴充到穩(wěn)定失敗模型中,需要加入一些新的謂詞和規(guī)則,ASP謂詞如表1所示。

表1 ASP謂詞Tab.1 ASP predicates

3.1 前綴和遞歸進程

前綴進程M具有如下形式:

M=x→N,意味著M首先完成事件x,接著進行N的行為,其中,α(x→N)=αN=αM。

根據(jù)進程的ASP謂詞推導(dǎo)進程的跡:

R1 trace(W,N,M):-exec(W,N,M)。

已知進程M的謂詞描述,利用ASP技術(shù)生成M的拒絕集,步驟為:

1)計算M的事件集;

2)由M的跡可推出M的可執(zhí)行的事件。

生成ASP規(guī)則如下:

R2 events(W,M):-trace(W,N,M)。

R3 events(W,N):-trace(W,O,N),behind (N,M)。

R4 behind(M,N):-exec(W,M,N)。

R5 perform(W,M):-trace(W,N,M)。

R6 refusal(W,M):-events(W,M),not exec (W,M)。

遞歸進程是一種特殊的前綴進程,例1證明了遞歸進程拒絕集由前綴進程拒絕集的生成方法生成。

例1 進程M的CSP描述為:

M=dseat→upStick→meal→dStick→useat→M。

對M進行謂詞表示:

{exec(dseat,m0,m).exec(upstick,m1,m0).exec(meal,m2,m1).exec(dstick,m3,m2).exec(useat, m,m3).totalp(m).}。

該進程描述與上述規(guī)則輸入到ASP回答集求解器DLV中,輸出回答集中包含M的穩(wěn)定失敗集的信息如下:

{totalp(m).refusal(upstick,m).refusal(meal, m).refusal(dstick,m).refusal(useat,m).}。

3.2 選擇進程

3.2.1 外部選擇

外部選擇進程具有如下形式:

M=(x→N|y→O)。

其執(zhí)行規(guī)則為:若環(huán)境選擇事件x,則進程執(zhí)行N;若環(huán)境選擇事件y,則進程執(zhí)行O。明顯地,M的跡需要包括所有可能發(fā)生的行為。

例2 顧客投入2元硬幣后,選擇售出大瓶飲料,或售出小瓶飲料后找零1元硬幣。該進程用CSP描述為:

V=(enter2c→large→V|enter2c→small→exit1c→V)。

圖2為進程V的跡及其ASP謂詞描述。其中, {extercho(large,v,v1)}表明進程在選擇運算時,已經(jīng)執(zhí)行了被選擇的事件。圖3為基于已定義的ASP謂詞計算進程V拒絕集的大致步驟。

圖2 進程V的跡及其ASP謂詞描述Fig.2 The traces and ASP predicates of process V

圖3 外部選擇V的拒絕集求解步驟Fig.3 The refusal sets solving steps of external choice V

因此,外部選擇進程的跡推導(dǎo)規(guī)則需要在上述規(guī)則上增加:

R7 trace(W,N,M):-extercho(W,O,M)。

外部選擇M的拒絕集與前綴算子類似,都是所有事件集與可執(zhí)行的事件集的差,差別在于前綴進程的可以執(zhí)行的事件只有一個,而M包括所有可能選擇的事件。M的拒絕集定義如下:

R8 refusal(W,M):-events(W,M),refusal (W,M),extercho(W,N,M)。

3.2.2 內(nèi)部選擇

內(nèi)部選擇進程具有如下形式:

表示進程M或按N的行為執(zhí)行,或按O的行為執(zhí)行,但它不允許由環(huán)境決定;相反,由進程內(nèi)部選擇。

例3 一臺自動售貨機在投入2元硬幣后,隨機選擇售出大瓶飲料,或售出小瓶飲料后找零1元硬幣。該進程可描述為:

圖4為進程S的跡及其ASP謂詞描述。其中, {intercho(large,s,s1,1)}除了表明進程在進行選擇時已經(jīng)執(zhí)行被選擇事件,還給出了編號,為后面計算拒絕集做準備。同時,如果只看可執(zhí)行的行為序列,其與例2中V一致。但S的拒絕集不止一個,且各不相同。圖5為基于已定義的ASP謂詞計算進程S拒絕集的大致步驟。已知內(nèi)部選擇的跡推導(dǎo)規(guī)則和外部選擇類似: R9 trace(W,N,M):-intercho(W,N,M,I)。進程M的拒絕集是N和O的拒絕集的組合,利用ASP技術(shù)生成步驟如下:

圖4 進程S的跡及其ASP描述Fig.4 The traces and ASP predicates of process S

圖5 內(nèi)部選擇S的拒絕集求解步驟Fig.5 The refusal sets solving steps of internal choice S

1)計算進程N和O的拒絕集;

2)由N和O的拒絕集構(gòu)成M的拒絕集。

因此,一般選擇進程的拒絕集求解規(guī)則如下:

R10 refusal(W,I):-events(W,M),not initial (W,I).initial(W,I):-intercho(W,N,M,I)。

R11 refusals(I,M):-intercho(W,N,M,I)。

3.2.3 一般選擇

進程M□N或按照進程M執(zhí)行,或按照進程N執(zhí)行,它提供給環(huán)境M和N的事件,由環(huán)境選擇具體哪個進程。若事件相同,其等同于M|N;若事件不同,等同于MN。

一般選擇的跡和非確定選擇的跡相同,其跡推導(dǎo)規(guī)則如下:

R12 trace(W,N,M):-genecho(W,N,M,I)。但拒絕集和非確定選擇的拒絕集不同,是N和O的拒絕集的交集,因此,其拒絕集求解規(guī)則如下:

R13 refusal(W,M):-refusal(W,N),refusal (W,O)。

3.3 并發(fā)組合

并發(fā)進程具有如下形式:

M=N‖O,要求進程N和O共同完成相同事件,分開完成不同的事件。根據(jù)CSP定義的并發(fā)規(guī)則,將M轉(zhuǎn)化為順序進程,即等價于前綴進程。因此,并發(fā)進程的跡推導(dǎo)規(guī)則為:

1)基于并發(fā)規(guī)則求解M的執(zhí)行序列;

2)根據(jù)M的執(zhí)行序列可計算M的跡。

M的拒絕集是2個子進程N和O拒絕集的并集,求解步驟如下:

1)由前綴進程的拒絕集定義分別生成子進程N和O的拒絕集;

2)由N和O的拒絕集計算M的拒絕集。

因此,并發(fā)進程的拒絕集推導(dǎo)規(guī)則如下:

R14 refusal(W,M):-events(W,M),refusal (W,M),not parallel(N,O,M)。

R15 refusal(W,M):-refusal(W,N),parallel (N,O,M)。

R16 refusal(W,M):-refusal(W,O),parallel (N,O,M)。

4 系統(tǒng)性質(zhì)LTL公式的ASP生成

性質(zhì)描述:售貨機在顧客投入一枚硬幣后,對顧客既提供咖啡的選擇,也提供茶的選擇。該性質(zhì)用LTL描述為:

?=□(coin?○(available tea∧available coffee))。其中,a??的形式是┐a∨(a∧?)的簡寫。進程C1滿足公式?,但進程C2不滿足。available可描述類似C1和C2的不同之處,但available并不表示阻止其他事件發(fā)生。如進程

C3=coin→(tea→C3□coffee→C3□chocolate→C3)同樣滿足?。

下述例子更能區(qū)分a和available a的不同之處(a包含available a):

主流的模型檢測工具采用CSP進程形式描述性質(zhì)規(guī)約,相較于LTL公式,其表達能力有限且通用性不強,特別是對活性的描述不足。為擴大活性驗證范圍,采用LTL進行規(guī)約。LTL公式可通過以下結(jié)構(gòu)生成:

1)原子謂詞。描述單個狀態(tài)。

2)連接詞。通常有析取∨、合取∧和否定┐。

3)時態(tài)詞?！?(“下一個?”):在下一個狀態(tài),?將成立;□?(“總是?”):在所有后繼狀態(tài)中,?成立;◇?(“最終?”):在后繼某些狀態(tài)中,?成立。

LTL公式說明了進程執(zhí)行需要滿足的性質(zhì)。當(dāng)M每步操作都滿足?時,記為:M??。

在CSP中,描述的是通信系統(tǒng),進程事件的發(fā)生取決于外部環(huán)境,因此,為了區(qū)分環(huán)境選擇和非確定性選擇,加入了事件的可能性(available)。定義以下原子公式。

a:環(huán)境執(zhí)行且只執(zhí)行事件a。

available a:環(huán)境可執(zhí)行事件a,但也可執(zhí)行其他事件。deadlocked:進程是死鎖的,等價于∧a∈Σ┐a。live:進程有活性,即非死鎖,等價于∨a∈Σ┐a。true,false:為真,或為假。

例4說明了加入available的原因。

例4 進程C1描述售貨機在接收一枚硬幣后,由顧客選擇咖啡或茶,而C2描述售貨機在接收一枚硬幣后,內(nèi)部選擇提供給顧客咖啡或茶。進程C1和C2用CSP描述為:

a→Chaos□b→Chaos滿足(a∧available b)∨(b∧available a)。

為簡化起見,定義LTL為:

?∈LTL::=true│false│a│available a│live│deadlocked;

│?1∧?2│?1∨?2│┐?│○?│□?│◇?。

給出穩(wěn)定失敗語義下,進程M的LTL公式對應(yīng)的ASP規(guī)則描述:

?=a??(M):-trace(a,N,M),not refusal(a, M);

?=available a??(M):-not refusal(a,M);

?=live??(M):-dlf(M),totalp(M);

?=deadlocked??(M):-not dlf(M);

?=?1∧?2??(M):-?1(M),?2(M);

?=?1∨?2??(M):-?1(M).?(M):-?2(M);

?=┐?1??(M):-not?1(M);

?=○?1??(M):-?1(N),next(N,M) ?(M):-deadlocked(M);

?=□?1??(M):-not f.f:-not?1(N),behind (N,M)?(M):-?1(N),not f.f:-?1(N), not?2(O),behind(N,O),behind(O,M);

?=◇?1??(M):-?1(N),behind(N,M)。

其中,系統(tǒng)活性live的ASP推導(dǎo)規(guī)則還包括:

dlf(M):-events(W,M),not refusal(W,M);

dlf(M):-exec(W,N,M),dlf(N);

dlf(M):-dlf(N),dlf(O),genecho(N,O,M)。

在分別給出進程M穩(wěn)定失敗模型的ASP規(guī)則以及穩(wěn)定失敗語義下LTL公式轉(zhuǎn)化為ASP的規(guī)則之后,檢測該進程性質(zhì)的流程為:

1)對M用ASP描述,加入其穩(wěn)定失敗語義的ASP規(guī)則,可生成穩(wěn)定失敗模型下的謂詞描述。

2)對給定性質(zhì)用LTL公式表示,根據(jù)對應(yīng)的ASP轉(zhuǎn)換通用規(guī)則,將其轉(zhuǎn)換為含性質(zhì)標(biāo)記的ASP規(guī)則。

3)將上述ASP謂詞及規(guī)則輸入到回答集求解器DLV中,運行該求解器,觀察得到的回答集中是否包含性質(zhì)標(biāo)記。

5 實驗分析

以思想家就餐模型為例,n位思想家圍著一張桌子,每對相鄰思想家中間有一根筷子,思想家只拿左邊或右邊的筷子,一位思想家只有拿到2根筷子才可進食。假設(shè)每位思想家都先拿左手邊的筷子,且只要他們拿起來,則直到進食后才能放下。思想家的行為用CSP描述為:

Mj=dseat→upStick.j→upStick.j→meal→dStick.j→dStick.j→useat→Mj。

以3位思想家為例,則j∈{1,2,3},將3位思想家進行并發(fā)運算構(gòu)成進程M。模型待驗證性質(zhì)如下:

1)一位思想家不能同一時間拿2根筷子;

2)該模型具有確定性;

3)該模型存在死鎖;

4)該模型是活性的;

5)只要某位思想家拿到筷子,他一定能吃到東西。

首先,用LTL公式表示上述性質(zhì),然后,根據(jù)LTL的轉(zhuǎn)化規(guī)則將其表示為ASP規(guī)則,待驗證性質(zhì)的LTL和ASP描述如表2所示。

表2 待驗證性質(zhì)的LTL和ASP描述Tab.2 LTL and ASP descriptions of the verified properties

把A∪B1∪B2∪B3∪B4∪B5以及規(guī)則R1~ R16和并發(fā)規(guī)則輸入到回答集求解器DLV中。圖6為該模型性質(zhì)驗證回答集。

圖6 該模型性質(zhì)驗證回答集Fig.6 Answer sets of the model properties verification

利用filter=f1,f2,f3,f4,f5語句使得回答集只顯示指定性質(zhì)。對于該并發(fā)系統(tǒng),在3位思想家同一時間拿起左手邊筷子時,開始陷入死鎖,每位思想家都無法進食,因此該系統(tǒng)不是活性的,只包含性質(zhì)標(biāo)記f1、f2、f3,不包含f4、f5,驗證結(jié)果與事實一致。

為避免死鎖的產(chǎn)生,規(guī)定第3位思想家先拿右手邊筷子:

M3=dseat→upStick.1→upStick.3→meal→dStick.1→dStick.3→useat→M3。

更改對應(yīng)的ASP描述為:

{exec(dseat,m31,m3).exec(upstick1,m32, m31).exec(upstick3,m33,m32).exec(dstick1,m34, m33).exec(dstick3,m35,m34).exec(useat,m3, m35).}。

此時更改集合A中的M3對應(yīng)的ASP謂詞描述,其他不變,輸入DLV求解器中,調(diào)整后的思想家就餐模型性質(zhì)驗證回答集如圖7所示。

圖7 調(diào)整后的思想家就餐模型性質(zhì)驗證回答集Fig.7 Answer sets of the modified dining philosophers model properties verification

性質(zhì)標(biāo)記f1、f2、f4、f5出現(xiàn)在回答集中,即調(diào)整后的思想家就餐模型不僅包含性質(zhì)f1和f2,且該模型是活性的(f4,f5),不包含性質(zhì)f3。

以上實例說明了基于ASP及穩(wěn)定失敗語義的并發(fā)系統(tǒng)性質(zhì)驗證方法的可行性和有效性,且可同時驗證多條性質(zhì)。

6 結(jié)束語

提出基于ASP及穩(wěn)定失敗語義的CSP并發(fā)系統(tǒng)模型驗證,減少了不同模型之間的轉(zhuǎn)換,利用LTL公式描述系統(tǒng)性質(zhì),具有更強的通用性。實驗結(jié)果表明,該方法可實現(xiàn)系統(tǒng)活性的驗證,且可驗證活性范圍更廣,同時,一次驗證多條性質(zhì),提高了驗證效率。下一步工作將考慮對穩(wěn)定失敗模型進行抽象,擴大待驗證系統(tǒng)規(guī)模。另一方面擴充到失敗發(fā)散模型,研究并發(fā)系統(tǒng)的活鎖問題。

[1] Hoare C A R.Communicating Sequential Processes[M/ OL].http://www.usingcsp.com/cspbooks,2004:1-112.

[2] Roscoe A W.The Theory and Practice of Concurrency [M].Prentice-Hall.United States:Prentice Hall,2005: 1-100,183-220.

[3] Isobe Y,Roggenbach M.A generic theorm prover of CSP refinement[J].Lecture Notes in Computer Science,2005(3440):108-123.

[4] Wei K,Heather J.Embedding the stable failures model of CSP in PVS[J].IFM,2005(3771):246-265.

[5] Roscoe A W.On the expressive power of CSP refinement[J].Formal Aspects of Computing,2005,17(2): 93-112.

[6] Murray T.On the limits of refinement-testing for model-checking CSP[J].Formal Aspects of Computing,2013 (2):219-256.

[7] Robinson T G,Armstrong T,Boulgakov P,et al.FDR3-A modern refinement checker for CSP[C]//20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,2014:1-14.

[8] Baral C.Knowledge Representation,Reasoning,and Declarative Problem Solving[M].Cambridge:Cambridge Univerdseaty Press,2003:5-64.

[9] Moshe Y V.Branching V.Linear time:final showdown [J].Lecture Notes in Computer Science,2011(2031):1-22.

[10] 趙嶺忠,司徒凌云,翟仲毅,等.基于ASP的CSP進程描述與組合研究[J].計算機科學(xué),2013,40(12):133-140.

編輯:梁王歡

CSP model checking based on ASP and stable failure semantics

Zuo Guizheng,Zhao Lingzhong
(School of Computer Science and Engineering,Guilin University of Electronic Technology,Guilin 541004,China)

Aiming at lack of activity description and the complexity of models transition of CSP model checkers,CSP model checking based on ASP and stable failure semantics is proposed.In this method,the properties are specified by linear temporal logic(LTL),the description of CSP system and LTL properties are implemented with answer set programming(ASP), then multiple properties are verified in one execution of ASP solvers.The experimental result shows that the method expands the scope of liveness properties based on stable failure model,and prevents transition from different models.

communication sequence process(CSP);linear temporal logic(LTL);stable failure semantics;answer set programming(ASP)

TP311

A

1673-808X(2015)05-0401-07

2015-03-18

國家自然科學(xué)基金(61262008,61100186);廣西可信軟件重點實驗室基金(KX201113)

趙嶺忠(1977-),男,河南社旗人,教授,博士,研究方向為形式化技術(shù)。E-mail:zhaolingzhong163@163.com

左貴征,趙嶺忠.基于ASP及穩(wěn)定失敗語義的CSP模型檢測[J].桂林電子科技大學(xué)學(xué)報,2015,35(5):401-407.