實時并發(fā)系統(tǒng)的PTSL模型檢測

王曉燕，韓嘯,2，彭君，劉淑芬

(1.吉林大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，吉林 長春 130012； 2. 吉林大學(xué) 學(xué)報編輯部，吉林 長春 130012)

實時并發(fā)系統(tǒng)的PTSL模型檢測

王曉燕1，韓嘯1,2，彭君1，劉淑芬1

(1.吉林大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，吉林 長春 130012； 2. 吉林大學(xué) 學(xué)報編輯部，吉林 長春 130012)

隨著實時并發(fā)系統(tǒng)的軟件規(guī)模越來越大、復(fù)雜性日趨增加，如何保證并發(fā)實時系統(tǒng)正確性和可靠性成為日益緊迫的問題。模型檢測技術(shù)采用自動化的驗證算法判斷系統(tǒng)是否具有某一性質(zhì)，它不僅包括對系統(tǒng)模型的遍歷以及基于圖形的分析方法，而且還需要大量的數(shù)值計算。本文把實時并發(fā)模型看成對并發(fā)博弈模型(CGS)的擴(kuò)展，在此基礎(chǔ)上添加了概率與時間性質(zhì)，提出了概率時間并發(fā)博弈結(jié)構(gòu)(PTCGS)。同時本文還提出了新的邏輯語言-概率時間策略邏輯(PTSL)，它顯式地把策略作為一階邏輯中的對象，從而使我們能夠以簡單而自然的方式指定PTCGS系統(tǒng)中的非零和屬性。PTSL模型檢測方法能夠讓設(shè)計者準(zhǔn)確知道模型是否滿足用戶的需求，從而提高系統(tǒng)的可靠性。最后，本文以ZeroConf協(xié)議為例來說明PTSL模型檢測方法的正確性。

模型檢測；概率時間并發(fā)博弈結(jié)構(gòu)；概率時間策略邏輯；概率時間自動機(jī)；區(qū)域圖；實時并發(fā)系統(tǒng)；博弈模型

實時并發(fā)系統(tǒng)被廣泛應(yīng)用在各領(lǐng)域中,例如并發(fā)和分布式實時軟件、離散事件模擬、通信網(wǎng)絡(luò)的建模等。這些系統(tǒng)中通常包含若干個并發(fā)構(gòu)件，這些構(gòu)件之間使用實時信號通信，并具有隨機(jī)性與不確定性。隨著計算機(jī)技術(shù)的發(fā)展，實時并發(fā)系統(tǒng)的軟件規(guī)模越來越大、復(fù)雜性日趨增加，如何保證其正確性和可靠性成為日益緊迫的問題，而且由于其內(nèi)在的非確定性，這個問題難度更大。

在為此提出的諸多理論和方法中，模型檢測(model checking)以其簡潔明了和自動化程度高而引人注目[1]。模型檢測作為形式化驗證的一種主流技術(shù)，它可以克服傳統(tǒng)軟件測試用例生成不完備的不足，同時具有驗證自動化的優(yōu)點，并且當(dāng)驗證的性質(zhì)不滿足時，能給出違背性質(zhì)的反例。模型檢測采用了嚴(yán)格的形式化方法對系統(tǒng)進(jìn)行驗證，因此比測試和仿真更能保證系統(tǒng)的正確性。模型檢測中常使用數(shù)學(xué)抽象模型對系統(tǒng)進(jìn)行建模，概率時間自動機(jī)(probabilistic timed automata， PTA)就是其中的一種[2-3]，由于它能同時表示概率性、不確定性和實時性，因此是模型檢測實時并發(fā)系統(tǒng)的有效工具。

模型檢測通過對狀態(tài)空間的窮舉搜索來判定系統(tǒng)是否具有所關(guān)心的性質(zhì)φ，但是隨著實時并發(fā)系統(tǒng)越來越多地應(yīng)用在一些對安全性、可靠性要求非常高的領(lǐng)域，如航空系統(tǒng)、電力系統(tǒng)、智能交通系統(tǒng)等，系統(tǒng)一旦發(fā)生故障所帶來的后果不堪設(shè)想，因此設(shè)計者需要確切知道在什么情況下系統(tǒng)會出現(xiàn)最壞或者最好的結(jié)果，這時候就需要通過模型檢測技術(shù)找到滿足特定性質(zhì)φ的某個策略或者最佳策略。

目前模型檢測主要用時序邏輯來刻畫所關(guān)心模型的性質(zhì)，常用的邏輯包括線性時態(tài)邏輯LTL(linear temporal logic)、概率計算樹邏輯PCTL(probabilistic computation tree logic)、概率時間計算樹邏輯PTCTL (probabilistic timed computation tree logic)、交替時間時態(tài)邏輯ATL(alternating-time temporal logic)等，當(dāng)系統(tǒng)中存在多個agent時，LTL、PCTL、PTCTL等不能夠明確描述每個agent對象所使用的策略[4-6]，而ATL又不能夠描述并發(fā)系統(tǒng)中的非零和邏輯[7-8]，于是Henzinger等提出了策略邏輯(strategy logic，SL)[9]，但是SL中缺少對不確定性以及時間的邏輯，因此本文提出概率時間策略邏輯(probabilistic timed strategy logic，PTSL)，把策略作為第一實體對象，能夠針對每個模型所使用的策略進(jìn)行描述，從而使我們能夠以簡單而自然的方式指定博弈系統(tǒng)中的非零和邏輯屬性。

本文的目的是在概率時間并發(fā)博弈結(jié)構(gòu)模型基礎(chǔ)上，為PTSL邏輯語言提供驗證方法。本文的主要貢獻(xiàn)如下:

1)在并發(fā)博弈結(jié)構(gòu)基礎(chǔ)上提出了概率時間并發(fā)博弈結(jié)構(gòu)模型；

2)提出的PTSL邏輯語言，它將策略和時態(tài)與概率度量相結(jié)合；

3)提出基于區(qū)域圖的PTSL模型檢測算法，并證明了區(qū)域圖中的路徑與PTA中的路徑的等價性。

1 相關(guān)工作

對實時并發(fā)系統(tǒng)的模型檢測可以分為2類：對并發(fā)模型的研究；對并發(fā)模型中使用的邏輯語言的研究。在實時并發(fā)系統(tǒng)中，通常使用一些控制策略，該策略模型與系統(tǒng)并發(fā)模型交互作用，因此完全可以把實時并發(fā)模型看成對博弈模型的擴(kuò)展。而目前博弈模型通常分為兩種類型：一種是輪流(turn-based)博弈模型[10]，在整個系統(tǒng)中，可以存在多個玩家，但是在每個狀態(tài)只能有一個玩家做出選擇，從而系統(tǒng)轉(zhuǎn)換到下一個狀態(tài)；還有一種是并發(fā)(concurrent)博弈模型[11]，同樣在整個系統(tǒng)中，可以存在多個玩家，但是在每個狀態(tài)多個玩家可以同時且獨立地做出選擇。Alfaro等[12]提出了時間博弈自動機(jī)，每個游戲者不僅可以選擇可能的轉(zhuǎn)換，同時還可以選擇轉(zhuǎn)換發(fā)生前的等待時間。Thomas Brihaye等[13]提出了時間并發(fā)博弈結(jié)構(gòu)TCGS，并使用新的邏輯語言TALTL進(jìn)行驗證。目前在并發(fā)模型中使用的邏輯語言的研究更豐富多彩。ATL是博弈模型中的一種典型，用來描述零和邏輯的語言[14]。Taolue Chen等[15]在ATL基礎(chǔ)上添加了概率算子，提出了PATL邏輯語言，Henzinger等提出了以策略為第一對象的非零和邏輯語言SL并給出了模型檢測算法，Christel Baier等[16]也在ATL基礎(chǔ)上提出了一種新的邏輯語言Stochastic Game Logic。

2 概率時間自動機(jī)與概率時間并發(fā)博弈結(jié)構(gòu)

2.1 時鐘與概率時間自動機(jī)

定義1 概率時間自動機(jī)(probabilistic timed automata, PTA)。PTA是一個八元組P=(L,l0,Act,χ,prob,inv,enab,L), 其中L表示自動機(jī)的位置集合;初始位置l0∈S；Act表示有限的動作集合;χ表示P中使用的時鐘集合；inv:L→C(χ)是環(huán)境函數(shù)，它為每個位置指定一個不變式；prob:L×Act→Dist(2χ×L)表示概率轉(zhuǎn)移函數(shù)，Dist(L)表示狀態(tài)L上的條件轉(zhuǎn)移的概率，且L上的所有條件轉(zhuǎn)移的概率和為1，即∑l∈Lθ(l)=1,θ:L→[0,1];enab:L×Act→C(χ)表示動作使能條件;標(biāo)簽函數(shù)L:L→2AP表示每個位置上的原子命題。

PTA中的符號狀態(tài)定義為二元組(l,v)，其中l(wèi)是符號狀態(tài)的位置信息，η是時鐘賦值且ηinv(l)。因此在符號狀態(tài)(l,η)上，要么有一定的時間流逝，要么某個動作m∈Act被執(zhí)行，即

μ(l′,η′)=∑{|prob(l,η)(X,l′)|X∈2χ∧

η′=η[X∶=0]|}

(X,l′)∈2χ×L表示支持動作m轉(zhuǎn)換的一條邊，在位置(l,η)上，所有的轉(zhuǎn)換邊記為〈e1,e2，…,em〉。從位置遷移的定義可以看出，一旦一個動作m被選擇，則時鐘會重置并隨機(jī)選擇后繼位置。

inv(l1,l2)=inv1(l1)∧inv2(l2)

enab((l1,l2),m)=

prob((l1,l2),m)=

L(l1,l2)=L1∪L2

2.2 概率時間并發(fā)博弈結(jié)構(gòu)

由于可以把實時并發(fā)模型看成對博弈模型的擴(kuò)展，本文首先給出由Henzinger等提出的并發(fā)博弈CGS模型的定義，如下所示。

定義3 并發(fā)博弈結(jié)構(gòu)(concurrent game structure，CGS)。CGS是一個8元組G=(Q,Q0,Σ,τ,Agt,Μ,Γ,Edg)，其中Q是CGS的有限狀態(tài)集合，Q0是初始狀態(tài)，Σ表示輸入與輸出動作集合，τ:Q×M→μ(M)是概率轉(zhuǎn)換函數(shù)，其中μ(M)是概率分布函數(shù)，Agt={a1,a2,…,ak}是系統(tǒng)中k個agent的集合，M是系統(tǒng)中所有agent可能的動作集合，而Γ定義了每個agent的動作，Edg:Q×Mk→τ表示狀態(tài)轉(zhuǎn)換表，它包含所有agent的每個狀態(tài)的狀態(tài)轉(zhuǎn)移函數(shù)。本文使用Edg(q,ma1,ma2,…,mak)表示狀態(tài)q上的所有agent的動作。

從上面的定義可以看出，在CGS中，由狀態(tài)qi轉(zhuǎn)換成狀態(tài)qi+1是由所有的agent共同作用的結(jié)果，這也就是說，每個agentaj∈Agt都會根據(jù)當(dāng)前的狀態(tài)qi選擇一個動作mj∈Mv(qi,aj)，因此狀態(tài)qi轉(zhuǎn)換成狀態(tài)qi+1需使用Edg(qi,a1,a2,…，ak)表示。

在CGS模型中缺少時鐘概念，因此本文對CGS模型進(jìn)行擴(kuò)展，在模型中添加時鐘，其定義如下所示。

定義4 概率時間并發(fā)博弈結(jié)構(gòu)(probabilistic timed concurrent game structure，PTCGS)。PTCGS是一個十元組T=(Q,Q0,Σ,χ,Inv,τ,Agt,Μ,Γ,Edg)，其中(Q,Q0,Σ,χ,Inv,τ)就是PTA，而Agt、Μ、Γ、Edg的含義與CGS中一樣。

因此在PTCGS系統(tǒng)中，每個agent都可以使用一個PTA來表示，整個PTCGS系統(tǒng)就是多個PTA的集合。

定義7 策略與聯(lián)合策略(strategy and coalition strategy)。策略通常表示系統(tǒng)中的agent在不確定性環(huán)境下如何在每個狀態(tài)選擇動作，從而找到滿足某個性質(zhì)的解決方案。agentai的策略σi是一個偏序函數(shù)，它將有限的路徑映射到概率分布函數(shù)，即σi:ρ→D(M)，且滿足當(dāng)m∈M(last(ρ))時，σ(ρ)(m)gt;0。聯(lián)合策略σA是指包含多個agent的策略集合。如果σA中包含所有的agent的策略，即A=Agt,則稱其為完全聯(lián)合策略，否則為不完全聯(lián)合策略。

3 概率時間策略邏輯語言

為了描述博弈系統(tǒng)的非零和邏輯，Chatterjee和Henzinger提出了策略邏輯(stragegy logic， SL)，該語言把策略作為第一實體對象，但缺少概率與時間特性。本文在SL基礎(chǔ)上提出概率時間策略邏輯(probabilistic timed strategy logic，PTSL)，其語法如下所示：

φ∷=p|ζ|φ|φ1∧φ2|

Φ∷=φ1∪≤kφ2|z.Φ

Λ∷=?x(a,x)Φ|?x(a,x)Φ|Λ1∧Λ2|Λ

ψ∷=P～λΛ

為了更好地描述時間性質(zhì)，在PTSL中引入了一個新的時鐘符號，稱之為公式時鐘，且χ∩=?，χ是PTA模型中的時鐘，稱為系統(tǒng)時鐘。ζ∈(χ∪)是一個時間區(qū)域Zone。z.φ表示從時鐘z=0的狀態(tài)開始搜索滿足φ的路徑，且z∈。?x·φ含義是任意策略x都滿足φ，而?x.φ表示存在一個策略x滿足φ，(a,x)φ是策略賦值公式，表示模型a使用策略x且滿足φ，～∈{lt;，?，gt;，?}，λ∈[0，1]，k∈R+，概率算子P表示滿足公式φ和界限符～λ的路徑的概率。在本文中，我們只考慮有兩個agent的并發(fā)實時系統(tǒng)，因此使用x1，x2，…，表示一個模型使用的策略，用y1，y2，…表示另外一個模型使用的不同策略。

因此使用PTSL語言可以表達(dá)如下的屬性，例如在ZeroConf協(xié)議中，發(fā)送者在發(fā)送信息后要求接收者要在1s內(nèi)接收到消息的概率大于等于99%，

P≥0.99[?x1?y1(s,x1)(r,y1)z.[s.l.=12∪

(r.l=4∧z≤1)]

定義8 擴(kuò)展的時間區(qū)域。由于在PTSL中存在公式時鐘變量z，因此本文將[η,I]稱為擴(kuò)展的時間區(qū)域，其中η是系統(tǒng)時鐘，I是公式時鐘。從而本文使用(l,[η,I])表示PTA中的狀態(tài)，稱為擴(kuò)展的符號狀態(tài)。

4 基于region graph的模型檢測算法

4.1 基本知識

對于時鐘變量x，用kx表示時鐘x的上界值。對于實數(shù)t，用frac(t)表示t的小數(shù)部分，用?t」表示t的整數(shù)部分。

定義9 時鐘等價(clock equivalence)。兩個時鐘賦值v和v′是等價的，記為v≈v′，當(dāng)且僅當(dāng)滿足下列所有條件：

1)對于每一個時鐘變量x，要么?v(x)」=?v′(x)」,要么v(x)gt;kx并且v′(x)gt;kx;

2)對于所有的時鐘變量x和x′，如果v(x)≤kx并且v′(x)≤kx，那么

①frac(v(x))=0當(dāng)且僅當(dāng)frac(v′(x))=0；

②frac(v(x))≤frac(v(x′))當(dāng)且僅當(dāng)frac(v′(x))≤frac(v′(x′))。

本文使用[v]表示時鐘v所屬的等價類，同樣可以將≈?jǐn)U展到符號狀態(tài)，使用〈l,[v]〉表示狀態(tài)相同，時間等價的等價類，稱其為區(qū)域(region)。由于在PTSL有公式時鐘，因此在TCGS系統(tǒng)中使用擴(kuò)展的符號狀態(tài)(l,[η,I])，而使用〈l,[η,I]〉表示擴(kuò)展區(qū)域。在擴(kuò)展區(qū)域α中，使用zone(α)表示α中的等價時間類。

在PTA模型G中存在多個狀態(tài)，有的狀態(tài)存在后繼狀態(tài)，與之對應(yīng)的區(qū)域也會有后繼區(qū)域，而由多個區(qū)域組成的模型稱為區(qū)域圖。

定義10 后繼區(qū)域(successor region)。擴(kuò)展區(qū)域β=〈l,[η′,I′]〉是α=〈l,[η,I]〉的后繼區(qū)域，當(dāng)且僅當(dāng)存在正數(shù)t∈,t′∈，當(dāng)〈l,[η′+t′,I′+t′]〉∈β,則對任意t≤t′,都有〈l,[η+t,I+t]〉∈α∪β，記為succ(α)=β。

定義11 區(qū)域圖(region graph)。與PTAP對應(yīng)的區(qū)域圖R是一個三元組R(P,Λ)=(R*,Steps*,L*)，其中R*表示擴(kuò)展區(qū)域的集合，對于任意擴(kuò)展區(qū)域α=〈l,[η,I]〉∈R*轉(zhuǎn)換函數(shù)Steps*包含以下3種類型的轉(zhuǎn)換。

1)時間遷移：當(dāng)succ([η,I])inv(l),則

2)位置遷移：如果存在概率p′∈prob(l)而且[η,I]滿足PTA中的位置轉(zhuǎn)換條件τl(p′)，則

3)自身循環(huán)

標(biāo)簽函數(shù)L*的定義如下所示：

L*〈l,[η,I]〉=L(l)∪

{pζ|[η,I]滿足ζ，ζ∈Z(χ∪)(Λ)}

由于在驗證過程中需要使用區(qū)域圖上的策略，其定義如下。

定義13 區(qū)域圖上的策略(adversary)。在區(qū)域圖中的策略σR將有限路徑ω*映射到概率p且p∈Steps*(last(ω*))。

下面介紹在區(qū)域圖上的PTSL滿足關(guān)系。

定義14 PTSL的滿足關(guān)系。給定區(qū)域圖(P,Λ)以及PTSL公式φ，則PTSL在上的滿足關(guān)系定義如下：

(l,[η,I])true，對于所有l(wèi),η,I均成立

(l,[η,I])p?p∈L*(l,[η,I])

(l,[η,I])φ1∧φ2?

(l,[η,I])φ1and(l,[η,I])φ2

(l,[η,I])φ?(l,[η,I])φ

(l,[η,I])Λ1∧Λ2?

(l,[η,I])Λ1and(l,[η,I])Λ2

(l,[η,I])Λ?(l,[η,I])Λ

(l,[η,I])φ1∪≤kφ2?存在整數(shù)i,j及路徑ω*，且ω*(i)φ1，且對于任意i≤j≤i+k，都有ω*(j)φ2。

以上定義的滿足關(guān)系與PCTL的滿足關(guān)系的定義基本相同，而PTSL中獨有的3個操作符——時鐘重置z、任意算子?以及存在算子?滿足關(guān)系定義如下。

(l,[η,I])z.φ?

(l,[η,I[z:=0]])σAφ

(l,[η,I])?x(a,x)Φ??x∈σanda∈

A,(l,[η,I])Φ

(l,[η,I])?x(a,x)Φ??x∈σanda∈

A,(l,[η,I])Φ

將帶有概率算子公式P～λΛ展開，可以得到公式(1)、(2)、(3)：

(l,[η,I])P≥λ?x?y(a,x)(b,y)Φ(1)

(l,[η,I])P≥λ?x?y(a,x)(b,y)Φ(2)

(l,[η,I])P≥λ?x?y(a,x)(b,y)Φ(3)

公式(1)～(3)的概率值以及σA的求解過程是本文驗證算法的核心。

4.2 驗證算法

本節(jié)將介紹基于區(qū)域圖的PTSL驗證算法。本文將該算法分為3步：1)構(gòu)建TCGS系統(tǒng)的區(qū)域圖；2)在區(qū)域圖上解析PTSL公式；3)在TCGS系統(tǒng)中找到滿足公式的路徑。

從PTA構(gòu)造區(qū)域圖的方法按照區(qū)域圖的定義就可以得到，本文不再給出轉(zhuǎn)換算法。本文重點介紹在區(qū)域圖上解析PTSL公式的過程,首先仍舊是構(gòu)建PTSL的語法樹。在語法樹上，葉節(jié)點代表原子命題，而內(nèi)部節(jié)點標(biāo)識PTSL中的操作符標(biāo)識包括∧,,∪≤k,P等，PTSL的驗證算法如下所示。

算法1 PTSL驗證算法

foreachφ′ in sub(φ)do

caseφ′=p: [φ′]:={(l,[η,I])|l∈Lamp;l∈L(p)}

caseφ′=θ: [φ′]:={(l,[η,I])|(l,[η,I])/θ}

caseφ′=θ1∧θ2:[φ′]:={(l,[η,I])|(l,[η,I])θ1∩(l,[η,I])θ2}

caseφ′=ζ: [φ′]:={(l,[η,I])|l∈L∧I∈pζ}

caseφ′=z.θ:

[φ′]:={(l,[η,ζ[z:=0]])|(l,[η,ζ])θ}

caseφ′=θ1∪≤kθ2:Until(θ1,θ2,≤k)

caseφ′=P～λ?x?y(a,x)(b,y)θ: [φ′]:=P1θ

caseφ′=P～λ?x?y(a,x)(b,y)θ:[φ′]:=P2θ

caseφ′=P～λ?x?y(a,x)(b,y)θ:[φ′]:=P3θ

…

PTSL與PCTL的不同之處在于存在以下幾個操作：時鐘重置z.φ、任意?x(a,x)·Φ以及存在?x(a,x)·Φ，因此對于PTSL中其他的操作符，例如,∧,∨,∪≤k等，都可以采用PCTL中原有的算法，這里不作詳細(xì)介紹。ζ是公式時鐘，pζ的定義在區(qū)域圖中已經(jīng)給出，表示滿足時間賦值的命題。依據(jù)PCTL語義，P～λΛ的計算方法如下所示：

從定義可以看出，求解P～λΛ的值的問題其實是求解極值的問題。依據(jù)這個思路，我們來敘述式(1)～(3)的計算過程。

為了敘述的方便，下面將～λ直接定義為≥λ。

從PTSL的滿足關(guān)系可知，式(1)的含義是，無論agenta和agentb使用任何策略，所找到的路徑的目標(biāo)狀態(tài)都滿足Φ且概率大于等于λ，因此λ是agenta和agentb使用聯(lián)合策略σA=(x,y)下所得的最小值。從而我們可以將式(1)轉(zhuǎn)換為求解最小值問題。式(2)中P≥λ?x?y(a,x)(b,y)Φ的含義是，agenta和agentb存在某個策略，所找到的路徑的目標(biāo)狀態(tài)滿足Φ且概率≥λ，這也就是說，找到一條滿足條件的路徑即可，因此可以將式(2)轉(zhuǎn)換為求解最大概率問題。式(3)的含義是無論agenta使用任何策略，agentb都會找到某個策略y使所找到的路徑的目標(biāo)狀態(tài)滿足Φ且概率≥λ。因為a可以使用任意策略，所以式(3)其實是求解最小概率問題。以上將式(1)～(3)求解概率≥λ的情形進(jìn)行了分析，而≤λ恰好是相反的情形，在這里不再贅述。有關(guān)在區(qū)域圖中尋找概率最優(yōu)解的方法與在MDP中的方法一樣，可以使用value iteration的方法查找整個模型中的概率最大最小值[17]。而公式時鐘z值的計算則是將找到的滿足θ的路徑中的各個區(qū)域的時間最大值相加起來即可。

當(dāng)在區(qū)域圖中找到了滿足條件的路徑ω*后，這并不是最終解，還需要在TCGS系統(tǒng)中構(gòu)建與ω*相對應(yīng)的路徑ω，另外還需要證明ω*與ω的概率是一樣的，這樣才能保證最終找到的路徑ω是正確的。

構(gòu)建ω過程采用遞歸方法，算法如下所示。

算法2 構(gòu)建w過程

BuildPathFromRG(R,ω*)

length∶=(|ω*|;i∶=0;ω∶=?;Trans:=?;

Whileilt;length

if(i=0) amp;(η0,I)∈[η0,I0]

ω:ω∪(l0,η0);

else

if (ηi,I+Dω(i))∈[ηi,Ii]

ω:=ω∪(li,ηi);

Trans:=Trans∪{(li-1,ηi-1),(mi,pi),(li,ηi)}

return (ω,Trans)

5 實驗與結(jié)果

本文以ZeroConf協(xié)議為例說明PTSL的模型檢測方法。ZeroConf協(xié)議是一種用于局域網(wǎng)內(nèi)自動生成可用IP地址的網(wǎng)絡(luò)技術(shù)。設(shè)備S連接網(wǎng)絡(luò)后，首先隨機(jī)地選擇一個IP地址，然后設(shè)備S會向網(wǎng)絡(luò)中的其他設(shè)備連續(xù)K次發(fā)送“這個IP地址是否已經(jīng)被占用”的詢問信息， 如果設(shè)備S沒有收到任何應(yīng)答，則它會使用該IP地址，否則只要收到過1個“IP地址被占用”的應(yīng)答，設(shè)備S就會重新選擇IP地址。本文使用的模型是由Cheshire等建立的MDP模型修改而來[18]，為environment模型添加了消息丟失的概率，表示網(wǎng)絡(luò)中的其他設(shè)備在應(yīng)答設(shè)備S的詢問時，發(fā)送的信息有可能發(fā)生丟失，本文使用參數(shù)plost表示。則sender模型和environment模型如圖1、2所示。

圖1 sender模型Fig.1 sender model

圖2 environment模型Fig.2 environment model

為了驗證模型，在Prism中重新設(shè)計實現(xiàn)了PTSL邏輯語言，并使用PTA模型表示并發(fā)實時系統(tǒng)中的agent，使用PTA的組合模型表示整個PTCGS模型。組合后的PTA模型轉(zhuǎn)換成區(qū)域圖后，狀態(tài)節(jié)點一共有631個，在本文中不能全部給出，本文只給出幾個關(guān)鍵節(jié)點的圖，如圖3所示。

圖3 區(qū)域圖模型片段Fig.3 Fragment of region graph model

圖3中每個節(jié)點的值如下所示：

l[0]=((s=0,probes=0,ip=0,coll=0,e=0),{x=0,y=0,x=y})

l[1]=((s=1,probes=0,ip=0,coll=0,e=0),{x=0,y=0,x=y})

l[2]=((s=3,probes=0,ip=1,coll=0,e=0),{x=0,y=20,x-y=-20})

l[3]=((s=3,probes=0,ip=1,coll=0,e=0),{x=1,y=20,x-y=-19})

l[4]=((s=3,probes=0,ip=1,coll=0,e=0),{x=2,y=20,x-y=-18})

l[5]=((s=3,probes=0,ip=2,coll=0,e=0),{x=0,y=20,x-y=-20})

l[6]=((s=3,probes=0,ip=2,coll=0,e=0),{x=1,y=20,x-y=-19})

l[7]=((s=3,probes=0,ip=2,coll=0,e=0),{x=2,y=20,x-y=-18})

l[8]=((s=3,probes=1,ip=1,coll=0,e=0),{x=0,y=40,x-y=-40})

l[9]=((s=3,probes=1,ip=1,coll=0,e=0),{x=0,y=39,x-y=-39})

l[10]=((s=3,probes=1,ip=1,coll=0,e=0),{x=0,y=38,x-y=-38})

l[11]=((s=3,probes=1,ip=2,coll=0,e=0),{x=0,y=0,x=y})

l[12]=((s=3,probes=1,ip=2,coll=0,e=1),{x=0,y=0,x=y})

首先求新入網(wǎng)的設(shè)備可以成功分配到未使用的IP的概率，使用PTSL的屬性公式為

P≥λ?x?y(a,x)(b,y)(true∪(s=6amp;ip=2))

表1為測試時的數(shù)據(jù)取值，從結(jié)果可以看出，當(dāng)網(wǎng)絡(luò)中節(jié)點數(shù)N值變化較大時，最后成功獲得IP地址的概率不會發(fā)生很大的變化。

表1 ZeroConf的實驗結(jié)果1

使用PTSL求解在大于等于T時間內(nèi)設(shè)備仍未成功分配到IP的概率的屬性公式為

P≥λ?x?y(a,x)(b,y)z.(!(s=6amp;ip=2)∧z≥T)

表2為測試時的數(shù)據(jù)取值，從結(jié)果可以看出，當(dāng)時間限界T較小時(≤10)，發(fā)生不能配置合適的IP的概率大一些，而時間限界T≥20時不能成功獲得IP地址的概率幾乎為0，完全符合ZeroConf協(xié)議的標(biāo)準(zhǔn)。

表2 ZeroConf的實驗結(jié)果2

6 結(jié)束語

本文在CGS模型基礎(chǔ)上添加了概率及時間約束，提出了一種新的并發(fā)模型PTCGS。并根據(jù)PTCGS特點，提出了新的邏輯語言PTSL，它在SL邏輯的基礎(chǔ)上添加了時間與概率特性，把策略作為第一實體對象，能夠針對每個模型所使用的策略進(jìn)行描述，從而使我們能夠以簡單而自然的方式指定PTCGS系統(tǒng)中的非零和邏輯屬性，并給出了基于區(qū)域圖的模型檢測算法。最后以ZeroConf協(xié)議為例來說明PTSL的模型檢測方法的正確性。

[1]CLARKE E, GRUMBERG O, PELED D. Model Checking[M]. Cambridge : MIT press， 1999: 5-60.

[2]BEAUQUIER D. On probabilistic timed automata[J]. Theoretical computer science, 2003, 292(1): 65-84.

[3]KWIATKOWSKA M, NORMAN G, SEGALA R, et al. Automatic verification of real-time systems with discrete probability distributions[J]. Theoretical computer science ,2002, 282: 101-150.

[4]CLARKE E, EMERSON A. Design and synthesis of synchronization skeletons using branching time temporal logic[C]//Proceedinns of the Workshop Logic of Programs.Newyork, US, 1981: 52-71.

[5]HANSSON H， JONSSON B. A logic for reasoning about time and reliability[J]. Formal aspects of computing, 1994, 6(5): 512-535.

[6]ALFARO de L. Temporal Logics for the Specification of Performance and Reliability[C]//Proc STACS’97.New York, US, 1997: 165-176.

[7]ALUR R, HENZINGER T A, KUPFERMAN O. Alternating-time temporal logic[J]. Journal of the ACM, 2002, 49: 672-713.

[8]CHATTERJEE K， HENZINGER T A. Strategy improvement for stochastic Rabin and Strett Games[C]//Proc DBLP 2006. Bonn, Germany, 2006: 375-389.

[9]CHATTERJEE K, HENZINGER T A, PITERMAN N. Strategy logic[J]. Information and computation, 2007, 208(6): 677-693.

[10]Basset N, Kwiatkowska M, Topcu U, et al. Strategy synthesis for stochastic games with multiple long-run objectives[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Germany, 2015:256-271.

[11]KRISHNENDU Chatterjee, LUCA de Alfaro, THOMAS A,et al. Strategy improvement for concurrent reachability and turn-based stochastic safety games[J]. Journal of computer and system sciences， 2013, 79: 640-657.

[12]ALFARO L de, FAELLA M, HENZINGER T, et al. The element of surprise in timed games[C]//14thInternational Conference on Concurrency Theory. Marceille, France ,2003: 144-158.

[13]THOMAS Brihaye, FRAN Cois, LAROUSSINIE, et al. Timed Concurrent Game Structures[C]//Proceedings of the 18th international conference on Concurrency Theory. Lisbon, Portugal, 2007: 445-459.

[14]RAJEEV A, THOMAS A, HENZINGER, et al. Alternating-time temporal logic[J]. Journal of the ACM， 2002 ,49(5): 672-713 .

[15]CHEN Taolue, LU Jian. Probabilistic alternating-time temporal logic and model checking algorithm[C]// Fourth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD), 2007. Haikou, China, 2007: 35-39.

[16]CHRISTEL Baier, TOMBrázdil, MARCUS Gr??er, et al. Stochastic game logic[C]//Conference: Quantitative Evaluation of Systems. Edinburgh, UK ,2007: 227-236.

[17]MARTA Kwiatkowska A , GETHIN Norman A , JEREMY Sproston B, et al. Symbolic model checking for probabilistic timed automata[J]. Information and computation, 2007, 205(2): 1027-1077.

[18]MARTA Kwiatkowska, GETHIN Norman, DAVID Parker, et al. Performance analysis of probabilistic timed automata using digital clocks[J]. Formal methods in system design, 2006, 29(1): 33-78.

王曉燕，女，1977年生，講師，博士，主要研究方向為軟件建模與驗證技術(shù)、軟件開發(fā)新方法。申請發(fā)明專利2項，并獲得2010年中國國家專利優(yōu)秀獎，2008年吉林省科技進(jìn)步一等獎，中國商業(yè)科技進(jìn)步二等獎。發(fā)表論文20余篇，其中被SCI收錄5篇。

韓嘯，男， 1981年生，編輯，博士研究生，主要研究方向為網(wǎng)絡(luò)協(xié)同、軟件建模和網(wǎng)絡(luò)技術(shù)。

彭君，男，1981年生，講師，博士，主要研究方向為模型驅(qū)動技術(shù)、構(gòu)件技術(shù)、軟件體系結(jié)構(gòu)。

PTSLmodelcheckingoftimedconcurrentsystem

WANG Xiaoyan1， HAN Xiao1,2， PENG Jun1， LIU Shufen1

(1.College of Computer Science and Technology, Jilin University, Changchun 130012, China; 2. Editorial Office on Journal, Jilin University, Changchun 130012, China)

With the increased scale and complexity of real-time concurrent software systems, ensuringtheir correctness and reliability has become a matter of urgency. Current model-checking technology uses an automated demonstration algorithm to judgesystem properties, which must include the traversal in the system model and graph-based analysis techniques as well asextensive numerical computations. In this paper, we consider the timed concurrency model as an extension of the concurrent game model (CGS) and addprobability and time properties to propose a new probabilistic timed concurrent game structure (PTCGS). We also propose a new logic language called probabilistic timed strategy logic (PTSL), which uses strategy as the object in the first-order logic to specify the nonzero-sum attributes in a simple and natural way. Lastly, we give an example usingthe ZeroConf protocol to demonstrate the correctness of the PTSL model checking method.

model checking; probabilistic timed concurrent game structure; probabilistic timed strategy logic; probabilistic timed automata; region graph; timed concurrent system; game model

10.11992/tis.201706008

http://kns.cnki.net/kcms/detail/23.1538.TP.20170728.1901.012.html

TP311

A

1673-4785(2017)05-0694-08

中文引用格式：王曉燕，韓嘯，彭君，等.實時并發(fā)系統(tǒng)的PTSL模型檢測J.智能系統(tǒng)學(xué)報， 2017, 12(5): 694-701.

英文引用格式：WANGXiaoyan,HANXiao,PENGJun，etal.PTSLmodelcheckingoftimedconcurrentsystemJ.CAAItransactionsonintelligentsystems, 2017, 12(5): 694-701.

2017-06-05. < class="emphasis_bold">網(wǎng)絡(luò)出版日期

日期：2017-07-28.

國家自然科學(xué)基金項目(61502196).

王曉燕. E-mail：wangxy@jlu.edu.cn.