Mediator的概率擴(kuò)展*

薛驍勇，孫 猛

(北京大學(xué)數(shù)學(xué)科學(xué)學(xué)院,北京 100871)

1 引言

在計(jì)算機(jī)科學(xué)和軟件工程飛速發(fā)展的今天，需要解決的問題的規(guī)模越來越大，系統(tǒng)模型和程序?qū)崿F(xiàn)的復(fù)雜程度也越來越高，對整個系統(tǒng)進(jìn)行直接分析和建模往往十分困難，甚至無法完成?；诮M件開發(fā)的基本思想是將整個系統(tǒng)分解成多個較為簡單的組件，每個組件有特定的結(jié)構(gòu)和功能，對每個組件分別建立模型，最后將各個組件的模型連接起來構(gòu)成整個系統(tǒng)的模型。它的優(yōu)點(diǎn)是對組件的建模比較簡單，不同的組件可以由不同的團(tuán)隊(duì)進(jìn)行處理，并且組件可被復(fù)用于不同的系統(tǒng)之中，從而加速開發(fā)過程。

與此同時，對軟件安全性的需求也日益增長。但是隨著軟件系統(tǒng)復(fù)雜程度的提高，對安全性的驗(yàn)證往往變得更加困難。為了應(yīng)對這樣的需求，建模語言Mediator[1,2]出現(xiàn)了。它是一門基于組件的形式化建模語言，采用層次化和模塊化的基本結(jié)構(gòu)，使用自動機(jī)作為最基本的模型單位，對模型進(jìn)行形式化描述。自動機(jī)可以被連接構(gòu)成系統(tǒng)，從而用于描述更加復(fù)雜的系統(tǒng)行為。系統(tǒng)也可以被視為更復(fù)雜系統(tǒng)中的組件進(jìn)行組合，從而形成一種層次化的模塊化結(jié)構(gòu)。

與PRISM[3]、UPPAAL[4]等形式化建模工具相比，Mediator不需要使用者有豐富的形式化領(lǐng)域的專業(yè)知識，更加方便被學(xué)習(xí)使用。目前對Mediator也有一些驗(yàn)證和代碼生成的工作，例如由Mediator代碼自動生成一些程序語言的代碼[2,5]，將Mediator模型自動轉(zhuǎn)換到PRISM模型從而能對用Mediator建立的模型進(jìn)行模型檢驗(yàn)[6]。

當(dāng)前版本的Mediator僅支持對確定性行為的刻畫，這已經(jīng)能描述很多問題了。但是，對于在某些條件下的問題，使用有概率的模型會是一個更好的解決方法，例如對于哲學(xué)家用餐問題，就存在不引入其它條件即可解決死鎖問題的算法[7]。為了刻畫有概率行為的模型，本文對Mediator進(jìn)行了概率方面的擴(kuò)展，加入了描述概率行為的語法，并討論了如何在擴(kuò)展后的語言中將一個多層的系統(tǒng)展開，轉(zhuǎn)換成單層的自動機(jī)。最后通過使用馬爾可夫決策過程MDP(Markov Decision Process)定義展開后自動機(jī)的語義，給出了展開前多層系統(tǒng)的語義定義。

很多時候僅僅給出模型的描述是不夠的，還需要對模型的正確性進(jìn)行驗(yàn)證。本文通過將Mediator模型自動轉(zhuǎn)換成PRISM模型，可以使用PRISM形式化建模工具中所帶有的模型檢驗(yàn)器來對Mediator中的模型進(jìn)行驗(yàn)證。對于擴(kuò)展前的Mediator模型到PRISM模型轉(zhuǎn)換，已經(jīng)有了比較完整的工作[6]，在此我們對其進(jìn)行相應(yīng)的擴(kuò)展，使其能夠支持?jǐn)U展后的Mediator語法，從而可以對具有概率行為的Mediator模型進(jìn)行驗(yàn)證。

本文的正文結(jié)構(gòu)如下：第1節(jié)對Mediator進(jìn)行基本的介紹；第2節(jié)給出Mediator描述概率行為的語法擴(kuò)充；第3節(jié)介紹在含有概率的情況下如何將一個多層的系統(tǒng)轉(zhuǎn)變成一個等價的單層自動機(jī)，并使用馬爾可夫決策過程刻畫這個自動機(jī)的語義；第4節(jié)對PRISM代碼的自動生成進(jìn)行一定的補(bǔ)充，并對一個比特交換協(xié)議的具體實(shí)例，用Mediator進(jìn)行建模并將其轉(zhuǎn)換成PRISM模型，使用相應(yīng)的模型檢驗(yàn)器對其進(jìn)行驗(yàn)證；最后第5節(jié)對本文工作進(jìn)行總結(jié)。

2 Mediator介紹

Mediator通過形式化的語法對單個組件進(jìn)行建模，然后通過各種連接部件將其進(jìn)行連接。Mediator采用了形式化的衛(wèi)式轉(zhuǎn)移對組件行為進(jìn)行描述。一個Mediator程序由類型系統(tǒng)、函數(shù)、自動機(jī)和系統(tǒng)構(gòu)成，其定義如下所示：

program ::=(typdef| function| automaton |system)

其中，typedef是Mediator的類型部分，它支持整型、有界整型、浮點(diǎn)數(shù)類型、布爾值、字符類型和枚舉常量等多種常用的數(shù)據(jù)類型。而且這些基本的數(shù)據(jù)類型可以被進(jìn)一步組合以形成一些更為復(fù)雜的數(shù)據(jù)結(jié)構(gòu)，如多元組、數(shù)組、列表等。一個變量在被聲明的時候除了必須給出它的數(shù)據(jù)類型，還可以使用init對其進(jìn)行初始化。

function是Mediator的函數(shù)部分，用來封裝一類操作。與一般程序語言中的函數(shù)相似的是，它有本地變量，并且通過執(zhí)行輸入變量和本地變量上的操作得到輸出變量的值。但它也有不同之處，Mediator中的函數(shù)體只包含賦值語句和返回語句，沒有其它的控制語句。

自動機(jī)automaton是Mediator最基本的組成單位。與一般常見的自動機(jī)模型有所不同，在Mediator中自動機(jī)沒有狀態(tài)概念，僅僅包含變量聲明和衛(wèi)式轉(zhuǎn)移，這也是為了使Mediator更易于被使用和學(xué)習(xí)而做出的調(diào)整。Mediator中的自動機(jī)通過端口與其它自動機(jī)或系統(tǒng)進(jìn)行變量值的傳遞，端口有輸入端口和輸出端口2種，輸入端口僅能接受外界的消息，輸出端口僅能向外界傳遞消息。一個端口有其本身的類型，以表示它所能傳遞的變量值的類型。并且端口在創(chuàng)建之時便帶有reqRead、reqWrite和value3個變量，前2個用于控制端口的打開或者關(guān)閉，最后1個則用來儲存?zhèn)鬟f的值。自動機(jī)是Mediator最基本的組成單元，所有行為都要通過自動機(jī)來實(shí)現(xiàn)，具體的自動機(jī)語法規(guī)則會在下一節(jié)中給出。

system是系統(tǒng)的部分。系統(tǒng)由自動機(jī)連接組合而成，系統(tǒng)本身也可以連接組合構(gòu)成更大的系統(tǒng)，系統(tǒng)部分的語法樹如表1所示。

Table 1 Syntax tree of systems in Mediator表1 Mediator中系統(tǒng)的語法樹

component和connection是系統(tǒng)最主要的2個部分。component是系統(tǒng)中的組件部分，使用之前定義的自動機(jī)或系統(tǒng)對系統(tǒng)中的組件進(jìn)行描述。connection也使用自動機(jī)或系統(tǒng)定義了其所在系統(tǒng)中的一些組件，并且確定系統(tǒng)中組件的端口如何連接。有時系統(tǒng)的構(gòu)造比較復(fù)雜，例如需要將多個自動機(jī)發(fā)出的消息進(jìn)行匯總或者將一條消息進(jìn)行廣播，此時可以通過在internal中定義一些節(jié)點(diǎn)來使這些關(guān)系變得更加清晰。

3 語法擴(kuò)展

自動機(jī)是Mediator語言中最基本的組成部分，是功能的實(shí)現(xiàn)。為了擴(kuò)展Mediator的表達(dá)能力，需要對其中自動機(jī)的表達(dá)能力進(jìn)行擴(kuò)展。Mediator中自動機(jī)基本的功能和構(gòu)成已經(jīng)在第2節(jié)進(jìn)行了基本的介紹，本節(jié)給出自動機(jī)的組成語法，如表2所示。

Table 2 Syntax tree of automatons in Mediator表2 Mediator中自動機(jī)的語法樹

一個自動機(jī)由端口、變量和衛(wèi)式轉(zhuǎn)移構(gòu)成，其中衛(wèi)式轉(zhuǎn)移是決定自動機(jī)行為的最主要部分。一個衛(wèi)式轉(zhuǎn)移由衛(wèi)式條件和執(zhí)行語句構(gòu)成，當(dāng)衛(wèi)式條件被滿足時，其所對應(yīng)的語句便會被執(zhí)行。執(zhí)行語句有2類：一類是賦值語句，對自動機(jī)的本地變量和端口所對應(yīng)的變量進(jìn)行操作；另一類是同步語句，表示在某個端口執(zhí)行同步操作。如果一個轉(zhuǎn)移包含了和外部端口進(jìn)行通信的同步語句，則稱為外部轉(zhuǎn)移，否則稱為本地轉(zhuǎn)移。

在Mediator自動機(jī)中，轉(zhuǎn)移是有優(yōu)先級的。同組轉(zhuǎn)移中排在前面的轉(zhuǎn)移相比后面的轉(zhuǎn)移具有更高的優(yōu)先級，即只有在前面的所有轉(zhuǎn)移的衛(wèi)式條件都不被滿足且后面轉(zhuǎn)移的衛(wèi)式條件都被滿足時，后面的轉(zhuǎn)移語句才會被執(zhí)行。如果一個自動機(jī)只包含單個衛(wèi)式轉(zhuǎn)移，則語句的執(zhí)行順序就已經(jīng)被確定下來，這個自動機(jī)就是一個確定性的自動機(jī)。為了描述非確定的行為，Mediator引入了轉(zhuǎn)移組的概念，即用group來表示一組轉(zhuǎn)移。group后面的大括號里可以包含多個衛(wèi)式轉(zhuǎn)移語句，一個group內(nèi)的不同轉(zhuǎn)移之間是沒有優(yōu)先級順序的，即當(dāng)有多個轉(zhuǎn)移的衛(wèi)式條件被同時滿足時，將會從這些衛(wèi)式條件所對應(yīng)的語句中隨機(jī)挑選一個執(zhí)行。與普通轉(zhuǎn)移類似，不同轉(zhuǎn)移組之間也存在優(yōu)先級順序，普通的轉(zhuǎn)移可以被看成僅有一個轉(zhuǎn)移的轉(zhuǎn)移組。

上面這種方法雖然可用于描述非確定性行為，但是還不能表示概率行為。為了對概率行為進(jìn)行描述，本文在之前規(guī)則的基礎(chǔ)上添加了帶有概率的衛(wèi)式轉(zhuǎn)移，轉(zhuǎn)移的每個分支都帶有一個數(shù)，代表選擇這個分支的概率。擴(kuò)展后的語法規(guī)則如表3所示。其中,prob即為在衛(wèi)式條件被滿足時后面語句被執(zhí)行的概率。如果在同一條件下有多個轉(zhuǎn)移分支，可以用逗號連接它們對應(yīng)的多個語句，每個語句都有自己的概率，所有語句的概率相加之和為1。如果一個轉(zhuǎn)移帶概率，那么其后面的執(zhí)行語句只能為賦值語句，即概率轉(zhuǎn)移必定是本地轉(zhuǎn)移。這一設(shè)置基本不影響Mediator的表達(dá)能力，因?yàn)橥秸Z句所在轉(zhuǎn)移的衛(wèi)式條件大多只涉及端口相關(guān)的變量，這樣的轉(zhuǎn)移一般與概率無關(guān)。

Table 3 Automaton’s syntax in extended Mediator表3 擴(kuò)展Mediator中自動機(jī)的語法

擴(kuò)展后的自動機(jī)可以由一個三元組來表示，即Automaton=〈Port,Variable,Transition〉。Port為端口的集合，Variable是本地變量的集合，transition是帶概率的轉(zhuǎn)移組的集合，單個轉(zhuǎn)移被視作只含一個轉(zhuǎn)移的轉(zhuǎn)移組。Variable中也包含2部分，一部分是本地變量，記作vloc，另一部分是端口所涉及的變量，記作vport。

將自動機(jī)進(jìn)行連接組合構(gòu)成系統(tǒng)這一部分和未擴(kuò)展的Mediator語言沒有區(qū)別，仍然按照第2節(jié)中系統(tǒng)的語法規(guī)則來生成。在這里也用多元組來給出一個系統(tǒng)的表示，System=〈Port,vport,Entity,Internal,Link〉。其中Port是系統(tǒng)和外界交互的端口;vport是端口相關(guān)的變量;Entity是大系統(tǒng)中所包含的子系統(tǒng)和自動機(jī)的集合，包括所有組件和連接件中的個體;Internal為內(nèi)部節(jié)點(diǎn)的集合;Link是連接的集合，記錄了端口、內(nèi)部節(jié)點(diǎn)之間是如何相連的。一個連接形如〈p1,p2〉，其中p1、p2是端口或內(nèi)部節(jié)點(diǎn)，二者必須類型相同，當(dāng)二者都是端口時，必須一個為輸入端口另一個為輸出端口。

4 語義擴(kuò)展

從第3節(jié)的擴(kuò)展語法規(guī)則可以看出，擴(kuò)展后的Mediator語言仍然是一個擁有層次結(jié)構(gòu)的模型。直接為這種結(jié)構(gòu)給出合適的語義定義是比較復(fù)雜的，所以本文考慮先將一個多層的系統(tǒng)展開，把它變成一個不具有層次結(jié)構(gòu)的自動機(jī)，這樣就只需要對一般的自動機(jī)確定其語義即可。

4.1 標(biāo)準(zhǔn)自動機(jī)

為了將一個系統(tǒng)變?yōu)樽詣訖C(jī)，需要將系統(tǒng)從最底層向上逐層展開，為了方便這種展開，需要引入自動機(jī)的標(biāo)準(zhǔn)形式。本文給出標(biāo)準(zhǔn)自動機(jī)的定義如下所示：

定義1(標(biāo)準(zhǔn)自動機(jī)) 如果一個自動機(jī)只含有一個轉(zhuǎn)移組，并且轉(zhuǎn)移組中的每個轉(zhuǎn)移都是標(biāo)準(zhǔn)的，則該自動機(jī)被稱為標(biāo)準(zhǔn)自動機(jī)。

在此定義中用到了標(biāo)準(zhǔn)轉(zhuǎn)移的概念，下面給出它的定義。

定義2(標(biāo)準(zhǔn)轉(zhuǎn)移) 對于一個非概率轉(zhuǎn)移，如果它的執(zhí)行語句以賦值語句為開始和結(jié)束，并且在執(zhí)行語句中賦值語句和同步語句交錯出現(xiàn)，那么它就是一個標(biāo)準(zhǔn)轉(zhuǎn)移。對于一個概率轉(zhuǎn)移，如果它的每個分支的執(zhí)行語句都滿足上述條件，那么它就是一個標(biāo)準(zhǔn)轉(zhuǎn)移。

如果一個系統(tǒng)的組件都是標(biāo)準(zhǔn)自動機(jī)，那么在將其轉(zhuǎn)換成自動機(jī)的過程中就無需考慮轉(zhuǎn)移的優(yōu)先級問題，因?yàn)槊總€組件都只有一個轉(zhuǎn)移組。下面給出把一個普通的自動機(jī)轉(zhuǎn)換成標(biāo)準(zhǔn)自動機(jī)的方法：

首先需要把一般的轉(zhuǎn)移轉(zhuǎn)換成標(biāo)準(zhǔn)轉(zhuǎn)移。對于一個非概率衛(wèi)式轉(zhuǎn)移g→s1,s2,…,sn，可以用2個操作將其變成標(biāo)準(zhǔn)轉(zhuǎn)移：(1)如果出現(xiàn)連續(xù)的賦值語句，可以將其合并為單個賦值語句；(2)如果有2個相鄰的同步語句，那么可在其中間插入一個不改變當(dāng)前所有變量值的賦值語句，例如可將一個變量的值賦給它自己。如果開始和結(jié)束的位置上不是賦值語句，那么可以將這樣的賦值語句插入到開始或結(jié)尾。

不斷重復(fù)這2個操作，可以將所有的非概率轉(zhuǎn)移轉(zhuǎn)換成標(biāo)準(zhǔn)轉(zhuǎn)移。而對于概率轉(zhuǎn)移，因?yàn)槠渲兄挥匈x值語句而沒有同步語句，所以不需要進(jìn)行這樣的轉(zhuǎn)換。

現(xiàn)在只需把同一個自動機(jī)的多個轉(zhuǎn)移組合并為一個轉(zhuǎn)移組。考慮一個自動機(jī)的轉(zhuǎn)移組如下：

TG1= {g1,1→S1,1,g1,2→S1,2,…,g1,r1→S1,r1}

TG2= {g2,1→S2,1,g2,2→S2,2,…,g2,r2→S2,r2}

?

TGn= {gn,1→Sn,1,gn,2→Sn,2,…,gn,rn→Sn,rn}

其中，TG表示的是轉(zhuǎn)移組，優(yōu)先級高的在前面。因?yàn)橥粋€轉(zhuǎn)移組中的轉(zhuǎn)移沒有優(yōu)先級順序，所以在這里要做的就是消去各個轉(zhuǎn)移組中的優(yōu)先級關(guān)系。注意到TGi中的轉(zhuǎn)移發(fā)生的條件是TG1到TGi-1中所有轉(zhuǎn)移的衛(wèi)式條件都不滿足并且轉(zhuǎn)移本身的衛(wèi)式條件滿足?？梢粤頶i=gi,1∧gi,2∧…∧gi,ri，則轉(zhuǎn)移gi,j→Si,j在合并后的轉(zhuǎn)移組中為g1∧…∧gi-1∧gi,j→Si,j。對原來所有的轉(zhuǎn)移都進(jìn)行這樣的轉(zhuǎn)換之后，即可將所有的轉(zhuǎn)移組合并為一個轉(zhuǎn)移組。上面示例最終得到的轉(zhuǎn)移組為：

TG1= {g1,1→S1,1,g1,2→S1,2,…,g1,r1→S1,r1,

至此已經(jīng)將一個普通自動機(jī)轉(zhuǎn)換成了標(biāo)準(zhǔn)自動機(jī)，其中的轉(zhuǎn)移沒有優(yōu)先級關(guān)系，這為下一步將系統(tǒng)展開成為自動機(jī)提供了便利。

4.2 系統(tǒng)展開成自動機(jī)

給定一個系統(tǒng)〈Port,vport,Entity,Internal,Link〉，其所有的子結(jié)構(gòu)都是標(biāo)準(zhǔn)自動機(jī)，我們要將這個系統(tǒng)展開成為一個自動機(jī)。Mediator中的自動機(jī)有3個要素：端口、變量和轉(zhuǎn)移，展開的關(guān)鍵也就是處理這3部分。

端口是與外界進(jìn)行交互的部分，在系統(tǒng)內(nèi)部組件進(jìn)行合并的時候不需要額外的操作，新的自動機(jī)的端口就是原來系統(tǒng)的端口。

對于變量，要將原系統(tǒng)各個組件中的變量合并到新的自動機(jī)中。對于各個組件的本地變量，為了避免來自不同組件的變量出現(xiàn)變量名重復(fù)的情況，需要對變量進(jìn)行重新命名，在其前面加上其所在自動機(jī)的名字。例如自動機(jī)A的本地變量state，在展開后的自動機(jī)中對應(yīng)的變量名為A_state。對于內(nèi)部節(jié)點(diǎn)i，添加i_reqRead,i_reqWrite,i_value3個變量到新的自動機(jī)中。對于各個組件的端口變量，也需要經(jīng)過更名后加入到新的自動機(jī)中，但區(qū)別是可以用Link中的連接減少一些端口變量。若〈p1,p2〉是一個連接，且p1和p2都不是系統(tǒng)的端口時，可以用一個端口替代另一個端口的出現(xiàn)；若二者有一個是系統(tǒng)的端口時，則用該系統(tǒng)端口替代另一個的出現(xiàn)，從而減少變量的數(shù)量。

最后考慮轉(zhuǎn)移，轉(zhuǎn)移分為內(nèi)部轉(zhuǎn)移和外部轉(zhuǎn)移2種。因?yàn)槊總€組件都是標(biāo)準(zhǔn)自動機(jī)，它們都只有一個轉(zhuǎn)移組，所以在合并的時候不會涉及到優(yōu)先級的問題。對于內(nèi)部轉(zhuǎn)移，因?yàn)樗鼈冎慌c其組件的行為有關(guān)，所以將變量名替換為更新后的變量名直接加入新自動機(jī)即可。由于概率行為只在內(nèi)部轉(zhuǎn)移中出現(xiàn)，因此對于外部轉(zhuǎn)移的處理和傳統(tǒng)的Mediator語言一樣[1]，利用依賴圖和拓?fù)渑判驅(qū)⑺心軌蛘系耐獠哭D(zhuǎn)移整合到一起再加入新的自動機(jī)即可。

4.3 自動機(jī)的語義

對Mediator中的一個自動機(jī)Automaton= 〈Port,Variable,Transition〉，本文用馬爾可夫決策過程來給出它的語義。馬爾可夫決策過程的定義[8]如下所示：

定義3(馬爾可夫決策過程) 馬爾可夫決策過程是一個四元組〈State,Act,→,s0〉。其中，State是狀態(tài)集合，Act是動作集合，s0是初始狀態(tài)，→是轉(zhuǎn)移的集合，它是State×Act×[0,1]×State的一個子集。

Mediator中的自動機(jī)沒有狀態(tài)，為了和馬爾可夫決策過程的狀態(tài)相對應(yīng)，本文通過自動機(jī)變量的值來生成狀態(tài)。用EV(Variable)表示自動機(jī)所有變量的所有可能值的集合，其中的一個元素是所有變量的一組可能的取值。這樣在自動機(jī)所對應(yīng)的馬爾可夫決策過程〈State,Act,→,s0〉中，State=EV(Variable)。初始狀態(tài)s0即為所有變量取初始值時對應(yīng)的狀態(tài)。

動作集合Act= {i}∪P(Port)，用來標(biāo)記在轉(zhuǎn)移過程中所涉及的端口，其中P(S)表示集合S的冪集；{i}表示轉(zhuǎn)移沒有涉及到任何端口，用來刻畫內(nèi)部轉(zhuǎn)移。

轉(zhuǎn)移集合→是State×Act×[0,1]×State的子集。在Mediator的自動機(jī)中執(zhí)行語句只有賦值語句和同步語句2種，而同步語句只標(biāo)識了哪些端口參與同步，而不改變變量的值，所以只有賦值語句可對變量的值進(jìn)行修改，即改變馬爾可夫決策過程的狀態(tài)。用s[var→value]表示在狀態(tài)s下將變量var的值改變成value所得到的新的狀態(tài)，用a(s)表示狀態(tài)s在執(zhí)行賦值語句a之后所達(dá)到的狀態(tài)。轉(zhuǎn)移的規(guī)則如圖1所示。

Figure 1 Semantics of extended Mediator圖1 擴(kuò)展Mediator的語義

圖1中的第1到第3條規(guī)則是刻畫外部環(huán)境對自動機(jī)的影響。因?yàn)橥獠凯h(huán)境的變化不可知，隨時可能請求讀取或?qū)懭肽硞€數(shù)據(jù)，為了能夠處理所有可能的情況，其相關(guān)的變量可以自由變化。第4條規(guī)則是針對外部轉(zhuǎn)移的，因?yàn)橥獠哭D(zhuǎn)移不會有概率行為，而且只有賦值語句會改變變量的值，所以僅僅需要將賦值語句作用到現(xiàn)有的狀態(tài)便可得到新的狀態(tài)。第5條規(guī)則為概率轉(zhuǎn)移對應(yīng)的語義，因?yàn)楦怕兽D(zhuǎn)移不涉及同步語句，所以把所有的賦值語句作用到現(xiàn)有的狀態(tài)上即可。

5 PRISM代碼生成和案例分析

5.1 PRISM代碼生成

PRISM是進(jìn)行概率模型檢驗(yàn)時常用的一款軟件，被廣泛應(yīng)用于通信協(xié)議、安全協(xié)議的建模分析等方面。我們希望將Mediator模型轉(zhuǎn)換成PRISM模型，從而對其進(jìn)行分析檢驗(yàn)。PRISM支持使用離散時間馬爾可夫鏈(DTMC)、連續(xù)時間馬爾可夫鏈(CTMC)、馬爾可夫決策過程(MDP)、概率時間自動機(jī)模型進(jìn)行建模。第4節(jié)使用馬爾可夫決策過程定義了Mediator的語義，所以在PRISM中的模型也是用馬爾可夫決策過程來進(jìn)行對應(yīng)。

對不包含概率轉(zhuǎn)移的Mediator模型到PRISM模型的轉(zhuǎn)換，已經(jīng)有了比較完整的工作[6]。其基本思想是將一個普通的分層的有多個組件的模型轉(zhuǎn)換成一個Mediator中的自動機(jī)，然后將這個自動機(jī)的變量和轉(zhuǎn)移分別轉(zhuǎn)換成相應(yīng)的PRISM模型。因?yàn)镻RISM不支持函數(shù)，支持的數(shù)據(jù)類型也要少于Mediator，為了使轉(zhuǎn)換后的代碼能被正確處理，此處考慮的模型中不含有這部分內(nèi)容。

對于加入概率轉(zhuǎn)移的Mediator模型轉(zhuǎn)換為PRISM模型的方法是類似的，也是先將系統(tǒng)轉(zhuǎn)換成單個自動機(jī)，通過上一部分定義的自動機(jī)的語義，得到自動機(jī)的馬爾可夫模型，最后依據(jù)這個模型得到對應(yīng)的PRISM模型。帶概率的Mediator模型和原來相比僅多了概率轉(zhuǎn)移，所以在此只需要將其生成對應(yīng)的PRISM代碼。PRISM中轉(zhuǎn)移的形式為[9]：

[]guard→prob1:update1+ … +probn:updaten

其中的update即為對變量進(jìn)行賦值更新的過程。在系統(tǒng)轉(zhuǎn)換成的自動機(jī)中，所有的轉(zhuǎn)移都在同一個轉(zhuǎn)移組中，相互之間沒有優(yōu)先級關(guān)系，可以直接將Mediator中的轉(zhuǎn)移對應(yīng)到PRISM中的轉(zhuǎn)移。

5.2 案例分析

本節(jié)使用Mediator描述比特交換協(xié)議ABP(Alternating-Bit Protocol)[8]，并將其轉(zhuǎn)換為PRISM代碼。在這里考慮的ABP模型結(jié)構(gòu)如圖2所示。

Figure 2 Structure of alternating-bit protocol圖2 比特交換協(xié)議的結(jié)構(gòu)

發(fā)信人和收信人通過2個信道進(jìn)行連接，其中一條為不可信信道，信息在其中可能會丟失，而另一條為可信信道，信息在其中不會丟失。通信開始，發(fā)信人通過不可信信道向接收者發(fā)送消息，消息中包含1 bit的控制比特(比如本次發(fā)送的是0)。如果消息沒有丟失，則收信人通過可信信道向發(fā)信人將該控制比特發(fā)送回去(在此為將0發(fā)送回去)。發(fā)信人接收到收信人的消息后開始發(fā)送下一條消息，該消息中包含和上一條相反的控制比特(這里將1發(fā)送出去)。如果信息在不可信信道中丟失了，或者是發(fā)信人沒有收到收信人的消息，發(fā)信人便不斷重復(fù)發(fā)送這條消息，直到收到收信人的消息為止。該系統(tǒng)的Mediator代碼如下所示：

system abp () {

components {

sender : Sender;

receiver : Receiver;

}

connections {

Sync(sender.uc,receiver.uc);

Sync(receiver.c,sender.c);

}

}

由于發(fā)信人通過不可信信道向收信人進(jìn)行發(fā)信，為了確保收信人能夠收到該條信息，讓其向收信人不斷發(fā)信直到收到收信人傳回來的消息，同時使用一個變量x來記錄發(fā)出的控制比特。對于收信人，使用一個變量y來確認(rèn)是否收到了含有正確控制位的信息，即收信人只接受控制比特和y相同的信息，這用來阻止還沒有向發(fā)信人反饋控制比特就收到了來自發(fā)信人的下一條信息。在這個系統(tǒng)中用了2個可靠的同步信道，其實(shí)現(xiàn)在文獻(xiàn)[10]中給出了。而不可信信道的特點(diǎn)選擇在收信人的組件中進(jìn)行描述。由此系統(tǒng)生成的PRISM代碼如圖3所示。

Figure 3 PRISM code generated from ABP model圖3 由ABP模型生成的PRISM代碼

下面借助PRISM自帶的模型檢驗(yàn)器對其進(jìn)行模型檢驗(yàn)。因?yàn)閺陌l(fā)信人到收信人的信道是不可信的，所以用如下規(guī)約來確保收信人一定能收到含特定控制比特的信息：

filter(forall,P>=1[Freceiver_z=true],sender_x=true)

這表示對任意滿足sender_x=true的狀態(tài)，最終到達(dá)滿足receiver_z=true的狀態(tài)的概率大于或等于1。這表示如果控制比特是1，則其一定能發(fā)送到收信人。把上述規(guī)約中的true改為false，則規(guī)約表示控制比特是0時收信人一定能收到。把二者合并進(jìn)行檢驗(yàn)，結(jié)果如圖4所示。

Figure 4 Verification result圖4 驗(yàn)證結(jié)果

圖4顯示這條規(guī)約是被滿足的，這說明通過足夠多次的發(fā)送，收信人最終一定能收到發(fā)信人發(fā)出的消息。

6 結(jié)束語

Mediator作為一種基于組件的形式化建模語言，其基于組件的特點(diǎn)使得它能夠適應(yīng)更大規(guī)模復(fù)雜系統(tǒng)的建模工作，并且對模塊進(jìn)行重用能夠有效簡化建模的過程。本文對Mediator做了概率方面的擴(kuò)展，使其能夠描述含有概率的行為，擴(kuò)展了Mediator的描述能力。此外還介紹了在擴(kuò)展之后如何將一個多層的系統(tǒng)轉(zhuǎn)換成沒有層次結(jié)構(gòu)的自動機(jī)，并且使用馬爾可夫決策過程給出了擴(kuò)展后Mediator的語義。除此之外，本文對原有的Mediator模型到PRISM模型的轉(zhuǎn)換器做了補(bǔ)充，使其能夠?qū)⒑懈怕市袨榈腗ediator模型轉(zhuǎn)化成PRISM代碼，從而能夠?qū)ζ涓怕市袨橄嚓P(guān)性質(zhì)進(jìn)行驗(yàn)證。