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

左貴征,趙嶺忠

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

左貴征,趙嶺忠

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

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

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

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

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

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

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

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

1 ASP簡(jiǎn)介

ASP是具有聲明特征的知識(shí)表示和推理的邏輯設(shè)計(jì)語言,它的基礎(chǔ)是回答集語義,可方便地用于非單調(diào)知識(shí)的表示和推理,且具有很強(qiáng)的聲明性,可對(duì)問題自動(dòng)求解,具有強(qiáng)大的知識(shí)表示能力。每個(gè)程序是一組規(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)準(zhǔn)規(guī)則;k=0的規(guī)則稱為完整約束;k=n的規(guī)則稱為事實(shí)。

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

2 模型檢測(cè)框架

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

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

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

1)CSP并發(fā)系統(tǒng)及其穩(wěn)定失敗模型的ASP描述和對(duì)應(yīng)規(guī)則。定義謂詞實(shí)現(xiàn)進(jìn)程的描述,根據(jù)這些謂詞定義對(duì)應(yīng)穩(wěn)定失敗模型(包括進(jìn)程的跡和拒絕集)的生成規(guī)則。其中,進(jìn)程包括基本進(jìn)程和并發(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)由進(jìn)程通過不同的算子組合而成,針對(duì)不同算子,分別定義對(duì)應(yīng)的謂詞描述及規(guī)則,從而通過組合實(shí)現(xiàn)并發(fā)系統(tǒng)的ASP描述及穩(wěn)定失敗模型的生成。

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

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

表1 ASP謂詞Tab.1 ASP predicates

3.1 前綴和遞歸進(jìn)程

前綴進(jìn)程M具有如下形式:

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

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

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

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

1)計(jì)算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)。

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

例1 進(jìn)程M的CSP描述為:

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

對(duì)M進(jìn)行謂詞表示:

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

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

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

3.2 選擇進(jìn)程

3.2.1 外部選擇

外部選擇進(jìn)程具有如下形式:

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

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

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

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

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

圖2 進(jìn)程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

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

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

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

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

3.2.2 內(nèi)部選擇

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

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

例3 一臺(tái)自動(dòng)售貨機(jī)在投入2元硬幣后,隨機(jī)選擇售出大瓶飲料,或售出小瓶飲料后找零1元硬幣。該進(jìn)程可描述為:

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

圖4 進(jìn)程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)計(jì)算進(jìn)程N(yùn)和O的拒絕集;

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

因此,一般選擇進(jìn)程的拒絕集求解規(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 一般選擇

進(jìn)程M□N或按照進(jìn)程M執(zhí)行,或按照進(jìn)程N(yùn)執(zhí)行,它提供給環(huán)境M和N的事件,由環(huán)境選擇具體哪個(gè)進(jì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ā)進(jìn)程具有如下形式:

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

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

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

M的拒絕集是2個(gè)子進(jìn)程N(yùn)和O拒絕集的并集,求解步驟如下:

1)由前綴進(jìn)程的拒絕集定義分別生成子進(jìn)程N(yùn)和O的拒絕集;

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

因此,并發(fā)進(jìn)程的拒絕集推導(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ì)描述:售貨機(jī)在顧客投入一枚硬幣后,對(duì)顧客既提供咖啡的選擇,也提供茶的選擇。該性質(zhì)用LTL描述為:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

為簡(jiǎn)化起見,定義LTL為:

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

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

給出穩(wěn)定失敗語義下,進(jìn)程M的LTL公式對(duì)應(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)。

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

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

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

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

5 實(shí)驗(yàn)分析

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

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

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

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

2)該模型具有確定性;

3)該模型存在死鎖;

4)該模型是活性的;

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

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

表2 待驗(yàn)證性質(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ì)驗(yàn)證回答集。

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

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

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

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

更改對(duì)應(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).}。

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

圖7 調(diào)整后的思想家就餐模型性質(zhì)驗(yàn)證回答集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。

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

6 結(jié)束語

提出基于ASP及穩(wěn)定失敗語義的CSP并發(fā)系統(tǒng)模型驗(yàn)證,減少了不同模型之間的轉(zhuǎn)換,利用LTL公式描述系統(tǒng)性質(zhì),具有更強(qiáng)的通用性。實(shí)驗(yàn)結(jié)果表明,該方法可實(shí)現(xiàn)系統(tǒng)活性的驗(yàn)證,且可驗(yàn)證活性范圍更廣,同時(shí),一次驗(yàn)證多條性質(zhì),提高了驗(yàn)證效率。下一步工作將考慮對(duì)穩(wěn)定失敗模型進(jìn)行抽象,擴(kuò)大待驗(yàn)證系統(tǒng)規(guī)模。另一方面擴(kuò)充到失敗發(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ìn)程描述與組合研究[J].計(jì)算機(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

國(guó)家自然科學(xué)基金(61262008,61100186);廣西可信軟件重點(diǎn)實(shí)驗(yàn)室基金(KX201113)

趙嶺忠(1977-),男,河南社旗人,教授,博士,研究方向?yàn)樾问交夹g(shù)。E-mail:zhaolingzhong163@163.com

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