（燕山大學(xué) 信息科學(xué)與工程學(xué)院， 河北 秦皇島 066004）

摘 要：

為了保證構(gòu)件在動(dòng)態(tài)演化時(shí)的行為一致性，提出了一種基于進(jìn)程代數(shù)的構(gòu)件模型，形式化描述了構(gòu)件及其對(duì)外交互協(xié)議，引入了對(duì)外主動(dòng)請(qǐng)求接口和內(nèi)部連接，并給出了行為一致性驗(yàn)證的規(guī)則和相關(guān)定理;然后給出了驗(yàn)證算法;最后，通過一個(gè)構(gòu)件化系統(tǒng)的實(shí)例來說明所提出方法的可行性。

關(guān)鍵詞：構(gòu)件； 動(dòng)態(tài)演化； 進(jìn)程代數(shù)； 行為一致性； 主動(dòng)請(qǐng)求接口

中圖分類號(hào)：TP311.5文獻(xiàn)標(biāo)志碼：A

文章編號(hào)：1001-3695(2009)04-1345-04

Research on behavioral consistency of component dynamic evolution based on process algebra

SHEN Li-min， MA Chuan， WANG Tao

（Information Science Engineering Institute， Yanshan University， Qinhuangdao Hebei 066004，China）

Abstract:To ensure behavioral consistency of components during dynamic evolution， defined a component model based on process algebra which formally specified the components and their interaction behaviors. Introduced the initiate request port and internal connection into the model， and then presented a set of rules and arithmetic to verify the behavioral consistency. Finally， presented an example of component-based system to illustrate the feasibility of the approach.

Key words：component; dynamic evolution; process algebra(PA); behavioral consistency; initiate request port



基于構(gòu)件的軟件工程(component-based software enginee-ring，CBSE)可有效地提高軟件開發(fā)質(zhì)量和效率，降低開發(fā)及維護(hù)成本。構(gòu)件演化是構(gòu)件系統(tǒng)維護(hù)的關(guān)鍵技術(shù)和研究熱點(diǎn)[1]，確保構(gòu)件系統(tǒng)的一致性是構(gòu)件演化的根本目標(biāo)。在一些如航空通信、工業(yè)控制、醫(yī)療等領(lǐng)域，停機(jī)演化所帶來的損失是巨大的甚至是無法忍受的，人們對(duì)動(dòng)態(tài)演化的需求日趨強(qiáng)烈。

構(gòu)件動(dòng)態(tài)演化是指構(gòu)件進(jìn)行在線變化并達(dá)到所希望形態(tài)的過程，其發(fā)生在軟件運(yùn)行期間，由一系列復(fù)雜的變化活動(dòng)組成，包括動(dòng)態(tài)添加、替換和刪除構(gòu)件，動(dòng)態(tài)配置系統(tǒng)結(jié)構(gòu)等。能否保證系統(tǒng)一致性，是衡量動(dòng)態(tài)演化正確與否的標(biāo)準(zhǔn)，如何保證系統(tǒng)一致性是動(dòng)態(tài)演化研究和實(shí)現(xiàn)中的首要問題，其中行為一致性的保證是其研究的重要內(nèi)容。行為一致性是指必須保證包括構(gòu)件交互行為和構(gòu)件本地行為在內(nèi)的構(gòu)件行為的完整性[2]。

目前，對(duì)構(gòu)件行為協(xié)議的研究主要有：基于CSP的SOFA[3]給出了軟件系統(tǒng)中構(gòu)件協(xié)議級(jí)可替換的必要條件，包含兩構(gòu)件組裝的可替換和構(gòu)件框架中的構(gòu)件可替換；Darwin給出了基于π演算[4]描述構(gòu)件交互協(xié)議的方式，但沒有給出驗(yàn)證構(gòu)件間協(xié)議級(jí)行為相容的方法；胡海洋等人[5]基于面向?qū)ο蠓缎偷捏w系結(jié)構(gòu)給出了組裝交互的構(gòu)件間協(xié)議級(jí)行為相容的一組驗(yàn)證規(guī)則。這些研究為構(gòu)件系統(tǒng)的一致性和構(gòu)件交互的正確性驗(yàn)證奠定了基礎(chǔ)，但沒有對(duì)構(gòu)件演化進(jìn)行探討。龔洪泉等人[6]基于π演算提出了保持系統(tǒng)一致性的演化規(guī)則，給出了構(gòu)件服務(wù)的端口類型和服務(wù)類型，但缺乏協(xié)議級(jí)行為相容性方面的考慮；黃崇德等人[7]基于Wright的軟件體系結(jié)構(gòu)描述語言描述構(gòu)件行為并在演化前確認(rèn)構(gòu)件的行為一致性，但提出的構(gòu)件語義匹配方法對(duì)語義的耦合度要求較高；Hameurlain[8]通過在新舊構(gòu)件間建立相容性和替換性，基于局部構(gòu)件行為的一致性來實(shí)現(xiàn)全局的系統(tǒng)行為的一致性，但降低了演化的靈活性。李長云等人[2]提出主動(dòng)請(qǐng)求接口和靜止?fàn)顟B(tài)等動(dòng)態(tài)演化相關(guān)概念并給出了保證行為一致性的算法，但缺乏形式化的表述。

本文基于進(jìn)程代數(shù)(PA)提出了一種構(gòu)件模型，形式化描述了構(gòu)件及其行為交互協(xié)議，給出了構(gòu)件動(dòng)態(tài)演化所需滿足的約束條件及行為一致性的驗(yàn)證算法。該模型既可以驗(yàn)證動(dòng)態(tài)演化時(shí)的行為一致性又可以驗(yàn)證演化后的構(gòu)件間行為相容性。

1 進(jìn)程代數(shù)

進(jìn)程代數(shù)是一種形式化的描述復(fù)雜并發(fā)系統(tǒng)的建模工具，是一種高層的描述語言，是支持并發(fā)分布系統(tǒng)的組合描述和其性質(zhì)形式化證明的代數(shù)語言。它以代數(shù)形式來描述模型，并為模型化系統(tǒng)定義了一套完整的語法和語義。

對(duì)于功能接口完全匹配的兩個(gè)交互構(gòu)件而言，其在運(yùn)行時(shí)演化仍會(huì)因行為協(xié)議的不相容而引發(fā)失敗。因此，構(gòu)件間能夠正確交互不僅需要定義符號(hào)級(jí)(signature level)的規(guī)范，還需要定義協(xié)議級(jí)(protocol level)的交互規(guī)范，即構(gòu)件間接口操作調(diào)用次序的約束與規(guī)范。因此，本文采用意大利學(xué)者M(jìn).Bernardo等人[9]提出的進(jìn)程代數(shù)作為形式化工具來描述與驗(yàn)證構(gòu)件的對(duì)外行為協(xié)議。其語法與語義規(guī)范定義如下：

定義1 系統(tǒng)中的進(jìn)程可用如下的范式形式化定義: 

E∷=0|a.E|E/L|E[φ]|E1+E2|E1‖sE2|A

0表示進(jìn)程已停止，不能再執(zhí)行任何動(dòng)作(action)；

a.E表示可執(zhí)行動(dòng)作a，然后轉(zhuǎn)換為進(jìn)程E；

E/L表示對(duì)于E中出現(xiàn)在L中相關(guān)動(dòng)作將被屏蔽其可被外界觀察的效果，即在運(yùn)行時(shí)將其轉(zhuǎn)換為進(jìn)程的不可見動(dòng)作τ；

E[φ]表示對(duì)E中的相關(guān)執(zhí)行動(dòng)作a進(jìn)行重標(biāo)號(hào)(relabel)，將其轉(zhuǎn)換為φ(a)；

E1+E2表示根據(jù)后續(xù)動(dòng)作所從屬的進(jìn)程作出選擇E1或E2；

E1‖E2表示進(jìn)程E1與E2對(duì)于從屬于集合S中的動(dòng)作同步執(zhí)行，而對(duì)于其他動(dòng)作則各自異步執(zhí)行；

A表示常量，可進(jìn)行這樣的定義AΔE。

2 構(gòu)件模型

構(gòu)件是指系統(tǒng)中具有相對(duì)獨(dú)立功能的實(shí)體。文獻(xiàn)[10]在構(gòu)件模型中增加了性能描述和性能保證機(jī)制。文獻(xiàn)[11]從組裝的需要出發(fā)，定義了由外部接口和內(nèi)部規(guī)約組成的構(gòu)件模型。文獻(xiàn)[5]則將行為協(xié)議引入構(gòu)件模型，研究構(gòu)件間在請(qǐng)求/提供接口上的協(xié)議級(jí)相容性。本文在已有的研究基礎(chǔ)上，基于進(jìn)程代數(shù)構(gòu)造構(gòu)件模型，描述了構(gòu)件的對(duì)外交互協(xié)議，同時(shí)引入了對(duì)外主動(dòng)請(qǐng)求接口和內(nèi)部連接，配合對(duì)外連接使構(gòu)件間的交互關(guān)系“有跡可循”，具有可追溯性。其接口分類如圖1所示。

定義2 擴(kuò)展了構(gòu)件對(duì)外主動(dòng)請(qǐng)求接口和內(nèi)部連接，并有行為協(xié)議描述的構(gòu)件模型可表述為這樣的一個(gè)七元組: C=〈IPC，IRC，IIRC，AC，LC，ILC，PC〉。

IPC為構(gòu)件C的對(duì)外提供接口集， IPC={Ite1，Ite2，…，Iten}。其中任何Itei∈IPC，Itei為C提供給外界調(diào)用的服務(wù)接口，它包含一組服務(wù)提供接口方法操作，即Itei={ai1，ai2，…，aini}。

IRC為C的對(duì)外請(qǐng)求接口集，任何Itei∈IIRC，Itej為C對(duì)外界所需的請(qǐng)求接口，它包含一組請(qǐng)求調(diào)用接口方法操作，即Itek={aj1，aj2，…，ajnj}。

AC為C的對(duì)外主動(dòng)請(qǐng)求接口集，任何Itek∈IIRC，Itek為C對(duì)外界所需的主動(dòng)請(qǐng)求接口，即任何Itei∈IPC∧IRC都不和Itek存在內(nèi)部連接關(guān)系。它包含一組主動(dòng)請(qǐng)求調(diào)用接口方法操作，即Itek={ak1，ak2，…，aknk}。

AC為構(gòu)件有窮接口動(dòng)作集，包括需求、服務(wù)和內(nèi)部動(dòng)作集：ARC，APC，AHC，且三者互不相交。

LC為有窮的構(gòu)件對(duì)外連接集，表達(dá)了本構(gòu)件與體系結(jié)構(gòu)中其他構(gòu)件間的組裝連接信息；每一構(gòu)件對(duì)外連接l1∈LC形如l1=〈RItei，PItei，LTi，LCi〉。其中RItei為構(gòu)件的一個(gè)請(qǐng)求接口；PItei為構(gòu)件的一個(gè)提供接口；RItei與PItei在語法上是完全匹配的；LTI={R+P}為該對(duì)外連接的類型，R表示本構(gòu)件通過li向所連構(gòu)件發(fā)送請(qǐng)求，P表示本構(gòu)件通過li向所連構(gòu)件提供服務(wù)；LCi為所連接的構(gòu)件。

ILC為C提供接口與請(qǐng)求接口之間或請(qǐng)求接口與請(qǐng)求接口之間存在的內(nèi)部連接關(guān)系，ILCIPC×IRC∧IRC×IRC。每一構(gòu)件內(nèi)部連接li∈ILC形如li=〈Itei，Itej〉。若構(gòu)件C為響應(yīng)從接口Itei接收的請(qǐng)求而從接口Itej向其他構(gòu)件發(fā)送新的請(qǐng)求，或構(gòu)件C為響應(yīng)從接口Itei請(qǐng)求其他構(gòu)件所返回的結(jié)果而從接口Itej向其他構(gòu)件發(fā)送新的請(qǐng)求。其中Itei∈IPC∧IRC稱為內(nèi)部請(qǐng)求接口，Itej∈IRC稱為內(nèi)部提供接口，則〈Itei，Itej〉∈ILC。

PC為構(gòu)件的行為協(xié)議，它通過PA進(jìn)行形式化定義，描述了本構(gòu)件對(duì)外交互行為協(xié)議約束與規(guī)范；PC對(duì)應(yīng)于這樣的（SC，ΓC）。其中：SC為構(gòu)件交互行為的有窮狀態(tài)集，Sinit、Sfina分別為初始化、終止?fàn)顟B(tài)；ΓcSC×AC×SC為對(duì)外交互行為的有窮狀態(tài)轉(zhuǎn)換集。

對(duì)于兩構(gòu)件Ci=〈IPCi，IRCi，IIRCi，ACi，LCi，ILCi，PCi〉和Cj=〈IPCj，IRCj，IIRCj，ACj，LCj，ILCj，PCj〉相連，若Ci請(qǐng)求調(diào)用Cj的提供接口Ite，則兩者的交互行為可表示為PCi‖ItePCj。這樣的Ite可稱為Ci，Cj間的共享請(qǐng)求/提供接口。不失一般性，本文設(shè)定相連構(gòu)件除出現(xiàn)在共享的請(qǐng)求/提供接口中的方法動(dòng)作同名以外，不同共享接口集內(nèi)的接口名與接口中的方法名互不相交。相連兩構(gòu)件間的共享接口集可表示為e(Ci，Cj)，它反映了相連構(gòu)件間通過一個(gè)或多個(gè)請(qǐng)求/提供接口進(jìn)行交互的關(guān)系，則與e(Ci，Cj)相對(duì)應(yīng)的構(gòu)件間同步接口方法集為a(Ci，Cj)=∪1≤k≤|e(Ci，Cj)|Itek(Itek∈e(Ci，Cj))；對(duì)于不相連的構(gòu)件間共享接口集e(Ci，Cj)=。e(Ci，Cj)與a(Ci，Cj)反映了相連構(gòu)件間通過請(qǐng)求/提供接口連接交互，且在接口方法上需同步運(yùn)行的關(guān)系。

多個(gè)構(gòu)件{C1，C2，…，Cn}Ci=〈IPCi，IRCi，IIRCi，ACi，LCi，ILCi，PCi〉可組裝成一定形式的體系結(jié)構(gòu)，體系結(jié)構(gòu)行為PM可形式化表示為PCi‖a(C1，C2)PC2‖a(C1，C3)∪e(C2，C3)PC3‖…‖a(C1，Cn)∪…∪a(Cn-1，Cn)Pn。

根據(jù)上面定義的構(gòu)件模型，可得以下定理：

定理1 若有PCi‖ItePCj，且有IIRCi=或?qū)θ魏蜪tek∈IIRCi有Itek≠Ite，則必有ILCi≠。

證明 反證法。設(shè)ILCi=，則構(gòu)件Ci的各接口之間無關(guān)聯(lián)，不存在為響應(yīng)一個(gè)接口的請(qǐng)求或結(jié)果而向另一個(gè)接口發(fā)送請(qǐng)求的情況，即除了對(duì)外主動(dòng)請(qǐng)求接口外不存在其他的對(duì)外請(qǐng)求接口。

a)若IIRCi=則構(gòu)件Ci無對(duì)外主動(dòng)請(qǐng)求接口，故構(gòu)件Ci無對(duì)外請(qǐng)求接口，與PCi‖ItePCj矛盾；

b)若對(duì)任何Itek∈IIRCi有Itek≠Ite則Ite為非主動(dòng)對(duì)外請(qǐng)求接口，即Ite必與構(gòu)件Ci的一個(gè)接口內(nèi)部連接，這與ILCi=矛盾。證畢。

該定理討論了主動(dòng)對(duì)外請(qǐng)求接口與內(nèi)部連接之間的關(guān)系。

3 行為一致性

構(gòu)件在運(yùn)行時(shí)刻通常會(huì)存在大量正在進(jìn)行的行為，包括構(gòu)件發(fā)送請(qǐng)求、接收應(yīng)答的交互行為以及構(gòu)件讀寫文件等本地行為。行為對(duì)系統(tǒng)狀態(tài)產(chǎn)生影響。對(duì)行為的任意中斷，可能導(dǎo)致系統(tǒng)處于不一致的狀態(tài)，破壞系統(tǒng)一致性。例如，刪除一個(gè)正在響應(yīng)請(qǐng)求的構(gòu)件，將導(dǎo)致發(fā)出該請(qǐng)求的構(gòu)件工作異常。中斷構(gòu)件的寫文件操作，也將導(dǎo)致系統(tǒng)I/O異常。因此，動(dòng)態(tài)演化必須保證包括了構(gòu)件交互行為和構(gòu)件本地行為在內(nèi)的構(gòu)件行為的完整性，即行為一致性。

3.1 行為一致性保證方法

為了保證構(gòu)件C在動(dòng)態(tài)演化時(shí)的本地行為一致性，需滿足以下條件：

a)構(gòu)件C當(dāng)前沒有參與自行啟動(dòng)的事務(wù)；

b)構(gòu)件C將來不會(huì)自行啟動(dòng)事務(wù)。

為保證本地行為一致性，構(gòu)件C從動(dòng)態(tài)演化開始到演化結(jié)束的有限時(shí)間T(T＞0)內(nèi)的狀態(tài)必須一直為Sinit或Sfina。

為了保證構(gòu)件在動(dòng)態(tài)演化時(shí)的交互行為一致性，需滿足以下條件：

a)構(gòu)件當(dāng)前沒有參與由其他構(gòu)件啟動(dòng)的事務(wù)；

b)構(gòu)件將來不會(huì)參與由其他構(gòu)件啟動(dòng)的事務(wù)，包括即將啟動(dòng)和已經(jīng)啟動(dòng)的需要構(gòu)件參與的事務(wù)。

為了保證交互行為一致性，構(gòu)件C從動(dòng)態(tài)演化開始到演化結(jié)束的有限時(shí)間T(T＞0)內(nèi)，所有對(duì)C主動(dòng)發(fā)送請(qǐng)求的構(gòu)件C′的狀態(tài)必須一直為Sinit或Sfina，這就阻止了C參與其他構(gòu)件啟動(dòng)的事務(wù)。

由以上的分析，定義構(gòu)件的靜止?fàn)顟B(tài)。

定義3 構(gòu)件C=〈IPC，IRC，IIRC，AC，LC，ILC，PC〉滿足如下條件時(shí)，處于靜止?fàn)顟B(tài)：

a)構(gòu)件C的狀態(tài)為Sinit或Sfina，即構(gòu)件C當(dāng)前沒有參與自行啟動(dòng)或由其他構(gòu)件啟動(dòng)的事務(wù)；

b)任何構(gòu)件C′=〈I′PC，I′RC，I′IRC，A′C，L′C，IL′C，P′C〉，C′≠C，若I′IRC≠，存在Ite∈I′IRC，有交互行為PC′‖ItePC或者PC′‖a(C′，C1)PC1‖a(C′，C1)∪a(C1，C2)PC2‖…‖a(C′，C1)∪…∪a(Ci-1，Ci)PC。其中i＞1，a(C′，C1)∈Ite，則C′的狀態(tài)為Sinit或Sfina。

定義中，條件b)保證了構(gòu)件C將來不會(huì)參與由其他構(gòu)件C′啟動(dòng)的事務(wù)，包括C′即將啟動(dòng)和已經(jīng)啟動(dòng)的需要構(gòu)件C參與的事務(wù)。

為了保證行為一致性，構(gòu)件C在動(dòng)態(tài)演化前必須進(jìn)入靜止?fàn)顟B(tài)。

定義3 給出的靜止?fàn)顟B(tài)，作為一種形式化驗(yàn)證規(guī)則來驗(yàn)證構(gòu)件在某一時(shí)刻是否可以動(dòng)態(tài)演化。但動(dòng)態(tài)演化是一個(gè)過程，所以演化前還得保證構(gòu)件C和C′在整個(gè)演化過程中不會(huì)自行啟動(dòng)事務(wù)，即在有限時(shí)間T(T＞0)內(nèi)C和C′的狀態(tài)一直為Sinit或Sfina。這可以通過構(gòu)件的管理機(jī)制實(shí)現(xiàn)，比如為每個(gè)構(gòu)件實(shí)現(xiàn)一個(gè)阻止自啟動(dòng)的方法，演化時(shí)由管理器調(diào)用該方法。

3.2 行為一致性驗(yàn)證算法

結(jié)合前面的定理和靜止?fàn)顟B(tài)定義，給出驗(yàn)證行為一致性的算法。

若對(duì)C=〈IPC，IRC，IIRC，AC，LC，ILC，PC〉進(jìn)行動(dòng)態(tài)演化：

a)檢查C的狀態(tài)。若為Sinit或Sfina，則轉(zhuǎn)b);否則不能演化。

b)遍歷搜索C的對(duì)外連接LC中對(duì)外連接類型LT=P所連接的構(gòu)件C′，即C通過對(duì)外連接（設(shè)接口為Itei）向C′提供服務(wù)。若存在C′，則轉(zhuǎn)c);否則可以演化，算法中止。

c)檢查C′的IIRC′。若IIRC′=或?qū)θ魏蜪tek∈IIRC′有Itek≠Itei，則轉(zhuǎn)d);否則轉(zhuǎn)e)。

d)檢查C′的ILC′。若ILC′為，則搜索C′的接口Itei所連接的構(gòu)件C″，以C″取代C′，轉(zhuǎn)c)；否則用Itei匹配ILC′中的內(nèi)部提供接口以找到其內(nèi)部請(qǐng)求接口，進(jìn)而由該內(nèi)部請(qǐng)求接口匹配LC′中的PIte(或RIte，兩者相同)，以找到與C′相連的構(gòu)件C″。以C″取代C′，以PItei取代Itei轉(zhuǎn)c)。

e)檢查C′的狀態(tài)。若為Sinit或Sfina，則可以演化；否則不能演化，算法中止。

該算法用來驗(yàn)證構(gòu)件某一時(shí)刻能否實(shí)施動(dòng)態(tài)演化。對(duì)于如何驅(qū)動(dòng)構(gòu)件C和C′進(jìn)入Sinit或Sfina狀態(tài)，要靠動(dòng)態(tài)配置等技術(shù)來實(shí)現(xiàn)。

4 應(yīng)用示例

以一個(gè)網(wǎng)上購書的構(gòu)件化系統(tǒng)為例來說明文中驗(yàn)證規(guī)則和算法的特點(diǎn)。在利用網(wǎng)絡(luò)購書時(shí)，有四類構(gòu)件參與其中，即用戶(user)、網(wǎng)上書店(bookShop)、圖書中介(bookBroker)和網(wǎng)絡(luò)銀行(bank)。在運(yùn)行過程中，bookShop在bookBroker進(jìn)行注冊(cè)(register)，當(dāng)有user需要圖書(getABook)時(shí)，bookBroker將查詢注冊(cè)的bookShop處是否有現(xiàn)貨(inStock)，若有bookBroker將進(jìn)行定貨(order)，并讓bookShop送貨(deliver)給user，并在bookShop的銀行賬戶上存入(deposit)書金。在如圖2所示的構(gòu)件系統(tǒng)中，構(gòu)件user、bank、bookShop都僅與構(gòu)件bookBroker相連，而它們之間不相連。User只有請(qǐng)求行為，bank只有提供行為，而bookBroker和bookShop間互有請(qǐng)求行為。User和bookShop分別有一個(gè)對(duì)外主動(dòng)請(qǐng)求接口Itebroker_user和Itebroker_shop。

interface BankAccount{

void login(in string accountNO);

float getBalance();

string deposit(in float amount);

string withdraw(in float amount);

void logout();

};

構(gòu)件bookShop提供的IDL接口bookShop描述如下：

interface Book_Shop{

struct BookRef{string ISBN; float price;}

booleaninStock(in string title， in string author);

void order(in BookRef b， out account a，out string purchaseID);

date deliver(in string purchaseID， in string rcpt， in string addr);

};

構(gòu)件bookBroker提供的IDL接口broker_User和broker_Shop描述如下：

interface Broker_User{

booleangetABook(in string author，

in string title， in float maxprice，

in string addr， out date when);

};

interface Broker_Shop{

void register(in Bookshop b);

void unregister(in Bookshop b);

};

該系統(tǒng)的四個(gè)對(duì)外連接中，構(gòu)件bookBroker為響應(yīng)從接口Itebroker_user接收的請(qǐng)求，而從接口Itebook_shop向構(gòu)件BookShop發(fā)送新的請(qǐng)求，故有內(nèi)部連接〈Itebroker_user，Itebock_shop〉；構(gòu)件bookbroker從接口Iteboook_shop向構(gòu)件bookShop發(fā)送請(qǐng)求后，為響應(yīng)請(qǐng)求結(jié)果，而從接口IteborkAccount向構(gòu)件bank發(fā)送新的請(qǐng)求，故有內(nèi)部連接〈Itebook_shop，ItebookAccount〉，如圖3所示。

根據(jù)定義2中的構(gòu)件模型，對(duì)構(gòu)件user、bookBroker、bookShop和bank的描述如下：

User=〈IPBU，IRBU，IIRBU，ABU，LBU，ILBU，PBU〉

IPBU：；

IRBU：{Itebroker_User}; IteBroker_User={getABook， getABook_r};

IIRBU:{IteBroker_User}; IteBorker_User={getABook， getABook_r}

ABU:(ARBU，APBU，AHBU);

ARBU:{getABook， getABook_r};

APBU:; AHBU: ;

LBU:{IteBroker_User， IteBroker_User， R， BookBroker};

ILBU:;

PBU:{PBUΔP[User]Init

P[User]InitΔgetABook. getABook_r. P[User]Fina

P[User]FinaΔ0};

BookBroker=〈IPBB，IRBB，IIRBB，ABB，LBB，ILBB，PBB〉

IPBB:{IteBroker_User，IteBroker_Shop}; IteBroker_User={getABook，

getABook_r}; IteBroker_Shop={register， unregister};

inStock_r， order， deliver， deliver_r}

IRBB: {IteBook_Shop， IteBookAccount}; IteBook_Shop={inStock， inSiock_r， orer， deliver， deliver_r};

IIRBB: ;

ABB: (ARBB， APBB， ARBB);

ARBB: {inStock， inStock_r， order， login， deposit， deposit_r， logout， deliver， deliver_r}; AHBB: ;

APBB: {getABook， getABook_r， register， unregister};

LBB: {〈IteBook_Shop， IteBook_Shop， R， BookShop〉，

〈IteBankAccount， IteBankAccount， R， Bank〉

〈IteBroker_Shop， IteBroker_Shop，P， BookShop〉，

〈IteBroker_User， IteBroker_User， P， User〉};

ILBB:{〈IteBrokr_User， IteBook_Shop〉，〈IteBook_Shop， IteBookAccount〉};

PBB:{PBBΔP[Broker]Init

P[Broker]InitΔregister， P[Broker]1

P[Broker]1ΔgetABook. P[Broker]2

P[Broker]2ΔinStock. inStock_r.

getABook_r. P[Broker]3

P[Broker]3Δorder.P[Broker]4+unregister. P[Broker]Fina

P[Broker]4Δlogin.deposit. deposit_r.

logout.deliver.deliver_r. P[Broker]1

P[Broker]FinaΔ0};

BookShop=〈IPBS，IRBS，IIRBS，ABS，LBS，ILBS，PBS〉

IPBS:{IteBook_Shop}; IteBook_Shop={inStock， inStock_r， order， deliver， deliver_r}

IRBS:{IteBook_Shop}; IteBroker_Shop={register， unregister}

IIRBS:{IteBroker_Shop}; IteBroker_Sho={register， unregister}

ABS: (ARBS， APBS， AHBS);

ARBS: {register， unregister}; AHBS: ;

APBS:{inStock， inStock_r， order， deliver， deliver_r};

LBS:{〈IteBroker_Shop， IBroker_Shop， R， BookBroker〉，

〈IteBook_Shop， IteBook_Shop， P， BookBroker〉};

ILBS: ;

PBS: {PBSΔP[Shop]Init

P[Shop]InitΔregister. P[Shop]1

P[Shop]1ΔinStock. inStock_r. P[Shop]2

P[Shop]2Δorder. deliver. deliver_r.

P[Shop]1+unregister. P[Shop]Fina

P[Shop]FinaΔ0};

Bank=〈IPBA， IRBA， IIRBA， ABA， LBA， ILBA， PBA〉

IPBA: {IteBankAccount}; IteBankAccount={login， getBalance，

getBalance_r， deposit， deposit_r， withdraw， withdraw_r， logout};

IRBA:;

IIRBA:;

ARBA，APBA，AHBA;

ARBA:; AHBA:;

APBA:{login， getBalance， getBalance_r， deposit， deposit_r， withdraw， withdraw_r， logout};

LBA:{〈IteBankAccount， IteBankAccount， P， BookBroker〉};

ILBA:;

PBA:{PBA ΔP[Bank]Init

P[Bank]InitΔlogin. P[Bank]1

P[Bank]1ΔgetBalance. getBalance_r.

P[Bank]1+deposit.deposit_r.

P[Bank]1+withdraw. withdraw_r.

P[Bank]1+logout. P[Bank]Fina

P[Bank]FinaΔ0};

如果對(duì)構(gòu)件bank進(jìn)行動(dòng)態(tài)演化，先檢查bank的狀態(tài)，若為P[bank]init或P[bank]fina，則搜索其對(duì)外連接LBA;否則不能演化。由LBA中的提供接口ItebankAccount找到與之相連的構(gòu)件bookBroker。因IIRBB=，檢查ILBB，用ItebankAccount匹配ILBB的內(nèi)部提供接口得其內(nèi)部請(qǐng)求接口Itebook_shop，再匹配LBB找到通過Itebook_shop與bookBroker連接的構(gòu)件bookShop。因IIRBS中的主動(dòng)請(qǐng)求接口Itebroker_shop≠Itebook_shop且ILBS=，于是由Itebook_shop又搜索到構(gòu)件bookBroker，用Itebroker_user匹配ILBB的內(nèi)部提供接口得其內(nèi)部請(qǐng)求接口Itebroker_user，從而找到通過Itebroker_user與bookBroker連接的構(gòu)件user，而Itebroker_user∈IIRBU，即構(gòu)件bank參與的事務(wù)由user啟動(dòng)。檢查user的狀態(tài)，若為P[user]init或P[user]fina，則可以演化，否則不能演化。

同理，可以得出構(gòu)件bookShop演化時(shí)需驗(yàn)證bookShop和user的Sinit或Sfina狀態(tài)；構(gòu)件bookBroker演化時(shí)需驗(yàn)證bookBroker、bookShop和user的Sinit或Sfina狀態(tài)；構(gòu)件user演化時(shí)只需驗(yàn)證其自身的Sinit或Sfina狀態(tài)即可。得出的結(jié)果與實(shí)現(xiàn)情況相符，表明文中所提途徑和算法是可行的。動(dòng)態(tài)演化完成后，利用文獻(xiàn)[5]中的構(gòu)件間的行為相容性驗(yàn)證規(guī)則進(jìn)行了驗(yàn)證，構(gòu)件間的行為是相容的。

5 結(jié)束語

本文基于進(jìn)程代數(shù)提出了一種構(gòu)件模型，形式化地描述了構(gòu)件及其對(duì)外行為協(xié)議，給出了構(gòu)件動(dòng)態(tài)演化所需滿足的約束條件。由于引入了對(duì)外主動(dòng)請(qǐng)求接口和內(nèi)部連接概念，使構(gòu)件交互關(guān)系有跡可循，尋找與演化構(gòu)件有交互關(guān)系的對(duì)外主動(dòng)請(qǐng)求接口變得容易。相比已有的構(gòu)件模型，該構(gòu)件模型既可以驗(yàn)證演化時(shí)的行為一致性，又可以驗(yàn)證演化后的構(gòu)件間行為相容性。從網(wǎng)上購書的示例可以看出，本文所提方法不僅可行而且是實(shí)用的。如何形式化描述構(gòu)件隨時(shí)間而演化的過程有待進(jìn)一步研究。

參考文獻(xiàn)：

[1]SZYPERSKI C. Component software：beyond object-oriented programming[M]. 2nd ed. Harlow:Addison-Wesley，2002.

[2]李長云，何頻捷，李玉龍.軟件動(dòng)態(tài)演化技術(shù)[M].北京:北京大學(xué)出版社，2007.

[3]PLASIL F， VISNOVSKY S. Behavior protocols for software components[J]. IEEE Trans on Software Engineering， 2002，28(11):1056-1076.

[4]MILNER R. Communicating and mobile systems: the π-Calculus[M]. Cambridge: Cambridge University Press， 1999.

[5]胡海洋，呂建，馬曉星，等.面向?qū)ο蠓缎腕w系結(jié)構(gòu)中構(gòu)件行為相容性研究[J].軟件學(xué)報(bào)，2006，17(6):1276-1286.

[6]龔洪泉，趙文耘，徐如志，等.基于Pi演算的構(gòu)件演化研究[J].電子學(xué)報(bào)，2004，32(12A):238-242.

[7]黃崇德，彭鑫，趙文耘.體系結(jié)構(gòu)動(dòng)態(tài)演化中的構(gòu)件行為分析[J].計(jì)算機(jī)工程與應(yīng)用，2007，43(10):87-92.

[8]HAMEURLAIN N. On compatibility and behavioral substitutability of component protocols[C]//Proc ofthe 3rd IEEE International Confe-rence on Software Engineering and Forma Methods. 2005:394-403.

[9]BERNARDO M， CIANCARINI P， DONATIELLO L. Architecting families of software systems with process algebras[J]. ACM Trans on Software Engineering and Methodology， 2002，11(4):386-426.

[10]盧炎生，柴永星，徐麗萍.基于XML的具有性能約束構(gòu)件的組裝技術(shù)[J].計(jì)算機(jī)應(yīng)用研究，2006，23(12):97-100.

[11]梅宏，陳鋒，馮耀東，等. ABC:基于體系結(jié)構(gòu)、面向構(gòu)件的軟件開發(fā)方法[J].軟件學(xué)報(bào)，2003，14(4):721-732.