基于進程代數(shù)的構(gòu)件動態(tài)演化行為一致性研究

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

摘 要：

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

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

中圖分類號：TP311.5文獻標志碼：A

文章編號：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ā)及維護成本。構(gòu)件演化是構(gòu)件系統(tǒng)維護的關(guān)鍵技術(shù)和研究熱點[1]，確保構(gòu)件系統(tǒng)的一致性是構(gòu)件演化的根本目標。在一些如航空通信、工業(yè)控制、醫(yī)療等領(lǐng)域，停機演化所帶來的損失是巨大的甚至是無法忍受的，人們對動態(tài)演化的需求日趨強烈。

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

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

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

1 進程代數(shù)

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

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

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

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

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

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

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

E[φ]表示對E中的相關(guān)執(zhí)行動作a進行重標號(relabel)，將其轉(zhuǎn)換為φ(a)；

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

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

A表示常量，可進行這樣的定義AΔE。

2 構(gòu)件模型

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

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

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

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

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

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

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

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

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

對于兩構(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請求調(diào)用Cj的提供接口Ite，則兩者的交互行為可表示為PCi‖ItePCj。這樣的Ite可稱為Ci，Cj間的共享請求/提供接口。不失一般性，本文設定相連構(gòu)件除出現(xiàn)在共享的請求/提供接口中的方法動作同名以外，不同共享接口集內(nèi)的接口名與接口中的方法名互不相交。相連兩構(gòu)件間的共享接口集可表示為e(Ci，Cj)，它反映了相連構(gòu)件間通過一個或多個請求/提供接口進行交互的關(guān)系，則與e(Ci，Cj)相對應的構(gòu)件間同步接口方法集為a(Ci，Cj)=∪1≤k≤|e(Ci，Cj)|Itek(Itek∈e(Ci，Cj))；對于不相連的構(gòu)件間共享接口集e(Ci，Cj)=。e(Ci，Cj)與a(Ci，Cj)反映了相連構(gòu)件間通過請求/提供接口連接交互，且在接口方法上需同步運行的關(guān)系。

多個構(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≠。

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

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

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

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

3 行為一致性

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

3.1 行為一致性保證方法

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

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

b)構(gòu)件C將來不會自行啟動事務。

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

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

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

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

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

由以上的分析，定義構(gòu)件的靜止狀態(tài)。

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

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

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將來不會參與由其他構(gòu)件C′啟動的事務，包括C′即將啟動和已經(jīng)啟動的需要構(gòu)件C參與的事務。

為了保證行為一致性，構(gòu)件C在動態(tài)演化前必須進入靜止狀態(tài)。

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

3.2 行為一致性驗證算法

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

若對C=〈IPC，IRC，IIRC，AC，LC，ILC，PC〉進行動態(tài)演化：

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

b)遍歷搜索C的對外連接LC中對外連接類型LT=P所連接的構(gòu)件C′，即C通過對外連接（設接口為Itei）向C′提供服務。若存在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)部請求接口，進而由該內(nèi)部請求接口匹配LC′中的PIte(或RIte，兩者相同)，以找到與C′相連的構(gòu)件C″。以C″取代C′，以PItei取代Itei轉(zhuǎn)c)。

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

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

4 應用示例

以一個網(wǎng)上購書的構(gòu)件化系統(tǒng)為例來說明文中驗證規(guī)則和算法的特點。在利用網(wǎng)絡購書時，有四類構(gòu)件參與其中，即用戶(user)、網(wǎng)上書店(bookShop)、圖書中介(bookBroker)和網(wǎng)絡銀行(bank)。在運行過程中，bookShop在bookBroker進行注冊(register)，當有user需要圖書(getABook)時，bookBroker將查詢注冊的bookShop處是否有現(xiàn)貨(inStock)，若有bookBroker將進行定貨(order)，并讓bookShop送貨(deliver)給user，并在bookShop的銀行賬戶上存入(deposit)書金。在如圖2所示的構(gòu)件系統(tǒng)中，構(gòu)件user、bank、bookShop都僅與構(gòu)件bookBroker相連，而它們之間不相連。User只有請求行為，bank只有提供行為，而bookBroker和bookShop間互有請求行為。User和bookShop分別有一個對外主動請求接口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òu)件bookBroker為響應從接口Itebroker_user接收的請求，而從接口Itebook_shop向構(gòu)件BookShop發(fā)送新的請求，故有內(nèi)部連接〈Itebroker_user，Itebock_shop〉；構(gòu)件bookbroker從接口Iteboook_shop向構(gòu)件bookShop發(fā)送請求后，為響應請求結(jié)果，而從接口IteborkAccount向構(gòu)件bank發(fā)送新的請求，故有內(nèi)部連接〈Itebook_shop，ItebookAccount〉，如圖3所示。

根據(jù)定義2中的構(gòu)件模型，對構(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};

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

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

5 結(jié)束語

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

參考文獻：

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

[2]李長云，何頻捷，李玉龍.軟件動態(tài)演化技術(shù)[M].北京:北京大學出版社，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].軟件學報，2006，17(6):1276-1286.

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

[7]黃崇德，彭鑫，趙文耘.體系結(jié)構(gòu)動態(tài)演化中的構(gòu)件行為分析[J].計算機工程與應用，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].計算機應用研究，2006，23(12):97-100.

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