基于Pi演算的構件行為兼容性研究

摘 要:構件行為的兼容性分析是研究構件動態交互過程中的重要問題，其研究結果可應用于構件替換、遷移、動態自適應演化等研究。為了保證構件在替換或組合之后系統仍能正常穩定運行，利用Pi演算對構件行為進行建模，并對多個構件行為間的兼容性進行驗證，提出了絕對兼容、相對兼容等理論，并運用兼容度來判定構件行為兼容性強弱，且通過實例進行分析說明。

關鍵詞:Pi演算; 構件行為; 行為交互; 兼容性; 兼容度

中圖分類號:TP311

文獻標志碼:A

文章編號:1001-3695(2010)02-0537-04

doi:10.3969/j.issn.1001-3695.2010.02.037

Research on Pi-calculus-based behavioral compatibility of components

ZHAO Chun-bo， WU Qing， HU Wei-hua

(College of Computer， Hangzhou Dianzi University， Hangzhou 310018， China)

Abstract:Making research on behavioral compatibility of components is an important issue when studing the dynamic interaction of them.The research result could be applied to the research of component replacement， migration， dynamic adaptive evolution and so on.In order to ensure the stability of the whole system after replacement or combination of component，this paper used Pi-calculus to model the component behavior，and verified the compatibility between two component behaviors.Besides， gave some definitions，such as absolute compatibility， relative compatibility and compatible degree which could be used to judge the compatibility strength. At last， made a concrete example to analyse the behavioral compatibility of components.

Key words:Pi-calculus; component behavior; behavioral interaction; compatibility; compatible degree

0 引言

目前，構件技術[1]已經成為軟件產業發展的關鍵技術之一，推行基于構件的軟件開發技術是當前軟件生產的世界潮流。其中，對于構件動態交互行為模型以及構件動態自適應組裝與演化的研究在基于構件的軟件開發領域中十分活躍。近年來，對于構件行為的形式化描述，以及在構件交互行為的一致性、相容性[2]等方面取得了一定的研究成果。仲輝等人[3]通過運用Pi演算來對行為進行形式化建模，但卻無法為兩個行為之間的等價性驗證提供支持。申利民等人[4]對構件動態演化行為一致性方面進行了一些研究，但是不能保證構件組合內部流程結構是否正確，交互過程中是否存在死鎖或不可達狀態，對構件行為兼容性的驗證工作存在不足。在對構件進行增加、刪除、替換、重組之后，為了確保系統的正常穩定運行，提高構件動態演化的自適應性，必須保證構件之間動態交互行為的兼容性。那些交互行為兼容性不高的構件很有可能導致整個系統出錯或崩潰等后果。針對這一問題，本文著重闡述了構件實體間交互行為的兼容性驗證。

本文的主要工作就是在汲取現有理論研究成果的基礎上，首先基于Pi演算這一進程代數來形式化地描述與定義了構件行為以及構件交互行為[5~7]，之后給出了組裝交互的兩構件在請求/提供接口上行為兼容的驗證規則及定理。根據構件交互行為兼容性的強弱將其劃分為絕對兼容與相對兼容，前者要求交互行為能夠在每條可能的交互路徑上均能正常完成任務，后者要求至少存在一條可行交互路徑。在此基礎上，基于Pi演算來判定構件交互行為的兼容性。最后，通過具體實例來分析并驗證構件交互行為的兼容性。

本文介紹了Pi演算的基本語法與操作語義，并講述了如何對構件行為、構件間交互行為進行形式化表達，提出了構件行為兼容性的相關理論與驗證規則，并通過具體實例來分析并驗證構件間交互行為的兼容性。

1 基于Pi演算的構件行為建模

1.1 Pi演算基本語法與操作語義

Pi演算是由Robin Milner提出的一種進程代數，是一種用于形式化描述和分析并發系統的計算模型。Pi演算是對CCS(calculus of communication system)的擴展。Pi演算的基本描述單元是進程和名稱。在Pi演算中，消息通道、變量、數據值等基本元素都表示為名稱，每個名稱都有一定的作用域范圍，并且在進程交互的過程中，其范圍可以隨著進程間的名稱傳遞而擴大或縮小。進程是系統中的通信實體。

定義1 設M是一個表示名稱的集合，用a、b、c、d…表示M中的元素;A是一個代理(或過程)集合，用P、Q、R等表示A中的元素，則Pi演算的語法可進行如下定義:

P::=0|δ.P|(vy)P|P+Q|P‖Q

|[x=y]P|A(x1，x2，x3，…，xn)|P

δ::=a?(x)|a!(x)|τ

其中:(vy)P中的y被稱為約束名稱，P是它的轄域。在P中出現的非約束名稱為自由名稱，P中的自由名稱集合表示為fn(p)，約束名稱的集合表示為bn(p)，P中名稱的集合表示為n(P)。δ的語法給出進程執行的三種操作，稱為前綴(prefixes)。進程通過執行這些基本動作而進行演化。具體操作符的直觀語義如下所示:

a)0表示空進程或進程操作的顯示結束。

b)δ.P表示先執行前綴操作，之后再執行P。前綴可分為輸入前綴、輸出前綴與亞前綴。輸入前綴a?(x)表示在通道a上接收數據x;輸出前綴a!(x)表示在通道a上發送數據x;啞前綴τ表示先執行內部不可見動作τ。

c)P+Q表示選擇執行P或Q。

d)P‖Q表示并發執行P與Q。

e)[x=y]P表示如果條件x=y成立，則執行P;否則，不執行任何操作。

f)A(x1，x2，x3，…，xn)表示執行A中的所有代理或過程。

g)P表示循環執行P。

Pi演算的操作語義是進程表達式的行為推演規則。在給定進程集合之后，它的常用遷移關系如下所示:

INPa?(x).Pa?(y)P{y/x}

OUTPa!(x).Pa!(x)P

TAUPτP

SUMPδP′P+QδP′+Q

COMMPa?(x)P′，Qa!(y)Q′P‖QτP′{y/x}‖Q′

PARPδP′P‖QδP′‖Q，bn(δ)∩fn(Q)=

上述遷移規則定義中A/B表示如果A成立，則能得出B。規則后面的邏輯表達式是整個規則成立的約束條件，如規則PAR成立的前提構件是bn(δ)∩fn(Q)=。

最常用的是前綴規則。INP、OUTP、TAU三個前綴規則規定，通過執行該前綴動作，進程可以遷移到P。而對于兩個并發執行的進程P和Q，若P可以通過動作前綴a?(x)遷移到P，而Q可以通過動作前綴a!(y)遷移到Q，那么根據COMM規則，可通過一個內部動作，使收發動作互相吸收抵消，遷移到P′{y/x}‖Q′。其中P在通道a上接收到Q發來的消息y之后，遷移到P′并且將P中用x表示的變量替換成接收到的y，而Q在通道a上發送消息y之后，自然遷移到Q′。SUM和PAR規則表示的是，若P能夠通過動作遷移到P′，那么P與另一進程Q的選擇組合或并行組合不影響P的遷移動作。

1.2 構件行為的Pi演算表達

構件行為與Pi演算中的進程有著與生俱來的相似性。構件行為通過服務請求端口和服務提供端口與外界進行交互，其交互主要體現在消息的收發上。Pi演算的進程同樣是通過其對外通道與外部環境進行消息傳輸，因此構件接口與進程的通道相對應，而構件行為操作所接收或發出的消息與進程在通道上接收或發送的消息相對應;構件行為交互引發的行為演進與進程在和外部環境進行交互時的每一步遷移相對應。可見，構件行為與Pi演算的進程有較一致的對應關系。因此，采用Pi演算這種進程代數來對構件行為進行形式化建模[8]。

根據消息的傳遞方式，構件原子行為可分為只發不收、只收不發、先發后收與先收后發。對于一個構件，將其構件行為用進程P表示，所有通信端口的集合表示為GT={gt1，gt2，…，gtn}，輸入消息的集合表示為Min={i1，i2，…，ix}，輸出消息的集合表示為Mout={o1，o2，…，oy}。在端口gtn輸入消息ix可表示成gtn?(ix)，在此端口輸出消息oy可表示成gtn!(oy)。那么，在通信端口gtm上只發不收、只收不發、先發后收與先收后發的構件原子行為可通過進程代數分別表示為

Psend=gtm!(oj，oj+1，…，ok-1，ok).0

Preceive=gtm?(ij，ij+1，…，ik-1，ik).π.0

Psend，receive=gtm!(oj，…，ok).gtm?(ij，…，ik).0

Preceive，send=gtm?(ij，…，ik).π.gtm!(oj，…，ok).0

下面通過一個實例來進行構件行為的Pi演算表達。

例如，一個用于實現貨物銷售的銷售商構件，它有三個輸入接口，即聯系購貨商的接口(contact)、接收訂購單的接口(order)，以及接收預購單的接口(pre-order)。構件還有四個輸出接口:庫存滿足需求的接口(sufficient)、庫存無法滿足需求的接口(insufficient)、發送配貨的接口(prepare)、發送取消配貨的接口(cancel)。圖1所示是銷售商構件的行為視圖。

分別設置每次輸入/輸出的通道名稱，將輸入contact(CNT)的通道命名為GT1，將輸入order(OD)的通道命名為GT2，將輸入pre-order(POD)的通道命名為GT3，將輸出sufficient(SUF)的通道命名為GT4，將輸出insufficient(ISUF)的通道命名為GT5，將輸出prepare(PP)的通道命名為GT6，將輸出cancel(CC)的通道命名為GT7。

根據Pi演算的基本語法，輸入CNT的操作可形式化表示為GT1?(CNT)。類似地，輸入OD與輸入POD的操作可分別形式化表示為GT2?(OD) 與GT3?(POD)。輸入SUF、ISUF、PP與CC可分別用Pi演算形式化表示為GT4?(SUF) 、GT5?(ISUF)、GT6?(PP)與GT7?(CC)。

若整個構件行為用進程PSC表示，貨物滿足需求時執行進程PSUF ，貨物不滿足需求時執行進程PISUF ，則可以把銷售商的構件行為表示為

PSC=GT1?(CNT).(PSUF+PISUF)

PSUF=GT4!(SUF).GT2?(OD).

(PPREPARE+PCANCEL)

PPREPARE=GT6!(PP).0PCANCEL=GT7!(CC).0

PISUF=GT5!(ISUF).GT3?(POD).0

2 構件行為的兼容性驗證

2.1 行為兼容性相關理論

構件行為兼容性[9，10]主要是針對多個構件之間的交互行為而言的，用于檢查構件交互行為能否正常完成相應的操作，以及會不會影響系統整體的穩定性與可行性。以下對一些兼容性相關概念進行簡要定義。

定義2 可行交互路徑。若構件A與構件B具有以下的交互行為:a)構件A通過接口gta1向B發送信息msg1，B通過接口gtb1接收msg1;b)構件B通過接口gtb2向A發送反饋信息msg2，A通過接口gta2接收msg2，從而完成行為交互。以上的交互行為可按照輸入/輸出序列msg1、msg2成功地從行為初始態演變成結束態，稱序列msg1、msg2為可行交互路徑。相反，如果B在接收到msg1后不發送msg2而直接結束，則A無法通過接口gta2收到對應的消息而無法完成操作，則稱序列msg1、msg2為不可行交互路徑。

定義3 絕對兼容。對于構件A與B之間行為交互的每一條可能交互路徑，如果均為可行交互路徑，則稱A與B絕對兼容。

定義4 相對兼容。對于構件A與B之間的行為交互，如果不滿足絕對兼容，卻至少存在一條可行交互路徑，則稱A與B相對兼容。

定義5 兼容度。對于構件A與B之間的行為交互路徑，如果存在m條可行交互路徑，而交互路徑總數為n，則稱A與B的兼容度為m/n。

可通過以上的定義來判定構件交互行為的兼容性。平常所說的構件行為兼容可以是絕對兼容或相對兼容。然而，那些對系統整體穩定性與正確性，以及子構件間交互行為兼容性要求較高的系統，往往需保證構件交互行為具有較高的兼容度，或直接要求是絕對兼容。

2.2 兼容性驗證的一般規則

在驗證行為兼容性時，往往涉及到多個構件間的行為交互。現以兩個構件間的行為交互為例來講解其一般規則。對于兩個以上的構件間行為交互可通過此規則來類推。

根據消息傳遞方式，兩個構件間的原子交互行為可能有以下幾種情況:均只發不收、均只收不發、一個發送一個接收。將兩個構件行為表示成進程P1與P2，通信端口分別表示成gt1與gt2，傳遞的消息表示成m1與m2。構件的交互行為可通過進程的并發執行來表達。以上三種情況的構件原子交互行為可表示如下:

P1‖P2=gt1!(m1).0‖gt2!(m2).0(1)

P1‖P2=gt1?(m1).0‖gt2?(m2).0(2)

P1‖P2=gt1!(m1).0‖gt2?(m2).0(3)

P1‖P2=gt1?(m1).0‖gt2!(m2).0(4)

對于式(1)，兩個構件都只進行消息的發送，而沒有對消息進行接收并處理，從而無法正常完成操作，因此不兼容。

對于式(2)，兩個構件都只進行消息的接收，而不能通過獲取相應的消息來完成操作，不存在可行交互路徑，因此也是不兼容的。

對于式(3)與(4)，兩構件分別進行消息的發送與接收。如果m1=m2，則可實現進一步演化:

P1‖P2m1或m20‖0=0

可見，通過消息的傳遞，構件可以完成各自的操作，因此是兼容的，其中消息序列m1或m2是可行交互路徑。但是如果m1≠m2，則仍然不能正常完成相應的操作，因此不兼容。

可對以上三種構件原子交互行為進行擴展，得到各種復雜的構件交互行為。

2.3 實例驗證

針對上面提到的銷售商構件，創建一個購買商構件，將它們進行組合，之后驗證兩個構件之間的交互行為兼容性。

購買商構件具有七個接口(包括三個輸出接口與四個輸入接口)。輸出接口包括聯系銷售商的接口(contact)、發送訂購單的接口(order)以及發送預購單的接口(pre-order);輸入接口包括接收庫存足夠的接口(sufficient)、接收庫存不足的接口(insufficient)、接收配貨信息的接口(prepare)、接收取消配貨的接口(cancel)。通道命名與銷售商構件類似。具體的構件行為視圖如圖2所示。

將購買商構件的構件行為用PPC1表示，則可將其形式化表示為

PPC1=GT1!(CNT).(PSUF1+PISUF1)

PSUF1=GT4?(SUF).GT2!(OD).

(PPREPARE1+PCANCEL1)

PPREPARE1=GT6?(PP).0

PCANCEL1=GT7?(CC).0

PISUF1=GT5?(ISUF).GT3!(POD).0

之后，可將銷售商構件與購買商構件進行組合[11]，如圖3所示。

構件之間的動態交互可看成是一個并發系統，同樣可以通過進程之間的并行組合來表示。購買商構件與銷售商構件之間的并行交互行為在Pi演算中的表達如下:

P(SC，PC1)=PSC‖PPC1=

(GT1?(CNT).(PSUF+PISUF))‖

(GT1!(CNT).(PSUF1+PISUF1))

可進行以下的演化:

P(SC，PC1)=PSC‖PPC1=

(GT1?(CNT).(PSUF+PISUF))‖

(GT1!(CNT).(PSUF1+PISUF1))CNT

(GT4!(SUF).GT2?(OD).

(PPREPARE+PCANCEL)+PISUF)‖

(GT4?(SUF).GT2!(OD).

(PPREPARE1+PCANCEL1)+PISUF1)SUF

(GT2?(OD).(PPREPARE+PCANCEL))‖

(GT2!(OD).(PPREPARE1+PCANCEL1))OD

(GT6!(PP).0+GT7!(CC).0)‖

(GT6?(PP).0+GT7?(CC).0)PP0‖0=0

同理，按照另外兩個輸入/輸出序列CNT、SUF、OD、CC與CNT、ISUF、POD，最后均變成空進程，可見三條交互路徑全是可行交互路徑，因此這兩個構件的交互行為是絕對兼容的。

若修改購買商構件，去除當銷售貨物庫存無法滿足需求時發送預購單的動作，以及購買商不接收從銷售商發來的配貨信息，而只接收取消配貨的信息，則它與銷售商構件之間的交互行為視圖如圖4所示。

若將修改后的購買商構件行為命名為PPC2，則可將其形式化表示為

PPC2=GT1!(CNT).(PSUF2+PISUF2)

PSUF2=GT4?(SUF).GT2!(OD).PCANCEL2

PCANCEL2=GT7?(CC).0

PISUF2=GT5?(ISUF).0

購買商構件與銷售商構件之間的并行交互行為在Pi演算中的表達如下:

P(SC，PC2)=PSC‖PPC2=

(GT1?(CNT).(PSUF+PISUF))‖

(GT1!(CNT).(PSUF2+PISUF2))

可進行以下演化:

P(SC，PC2)=PSC‖PPC2=

(GT1?(CNT).(PSUF+PISUF))‖

(GT1!(CNT).(PSUF2+PISUF2))CNT

(PSUF+GT5!(ISUF).GT3?(POD).0)‖

(PSUF2+GT5?(ISUF).0)ISUF

(GT3?(POD).0)‖0

可見，當銷售商構件向購買商構件發送庫存不足信息ISUF之后，由于銷售商構件無法接收到從購買商發送來的預購單信息POD，無法完成正常的交互。然而，構件交互過程中存在輸入/輸出序列CNT、SUF、OD、CC，可以使得交互行為正常完成，即存在可行交互路徑。構件行為PSC與PPC2之間的交互屬于相對兼容。

之后計算這兩個構件交互行為的兼容度。對于銷售商構件，在與購買商構件進行行為交互時總共有三條可執行路徑:CNT、SUF、OD、PP;CNT、SUF、OD、CC;CNT、ISUF、POD。它在與購買商構件進行交互時只有一條可行交互路徑，即CNT、SUF、OD、CC。因此，這兩個構件交互行為的兼容度為1/3。

3 結束語

本文先利用構件行為與Pi演算中進程的相似性，論述了如何運用Pi演算這一進程代數來對構件行為以及構件并行交互行為進行形式化建模;之后提出一些用于判定構件交互行為兼容性的定義，包括可行交互路徑、絕對兼容、相對兼容，以及兼容度概念;最后，通過具體實例來驗證構件交互行為的兼容性，包括創建兩個構件，定義各自的構件行為視圖與行為交互視圖，并對它們的構件交互行為進行Pi演算形式化表達，檢查每條交互路徑是否為可行交互路徑，判定它們在行為交互過程中的兼容性(絕對兼容還是相對兼容)，并計算其兼容度。通過對構件交互行為兼容性的驗證，可以較有效地避免由于構件的增加、刪除、替換、遷移、重組等操作而影響系統的正常穩定運行，確保系統整體質量。然而，構件交互行為的強兼容性不僅以高兼容度的形式來體現，還可能以系統的高性能、高可靠性、高響應速率等方面來體現。本文在驗證構件行為兼容性時尚未考慮到這些因素，需進一步完善。

下一步的工作包括:更深入研究構件交互行為的兼容性，除了考慮構件交互行為的兼容度之外，綜合考慮系統的運行效率與執行穩定性，并形成一個統一的標準驗證體系，為實現普適環境下構件的動態自適應交互作準備。

參考文獻:

[1]韓丁，沈建京，萬芳，等.基于SOA的服務構件封裝技術研究[J].計算機工程與設計，2009，30(7):1756-1759.

[2]殷昱煜，李瑩，鄧水光，等.Web服務行為一致性與相容性判定[J].電子學報，2009，37(3):433-438.

[3]仲輝，王維平，黃炎炭，等.一種基于π演算的行為建模形式化方法[J].系統工程理論與實踐，2009，29(5):175-185.

[4]申利民，馬川，王濤.基于進程代數的構件動態演化行為一致性研究[J].計算機應用研究，2009，26(4):1345-1348，1352.

[5]陳波，李舟軍，陳火旺.構件模型研究綜述[J].計算機工程與科學， 2008，30(1): 105-109.

[6]GAO Jing，LAN Yu-qing， GUO Shu-hang， et al. A new modeling method of component interaction behavior[C]//Proc of World Congress on Intelligent Control and Automation (WCICA).2008:4773-4778.

[7]薛崗，姚紹文，LU J.基于Pi演算的工作流模式描述[J].計算機科學，2008，35(7):191-194.

[8]ACCIAI L， BOREALE M. Spatial and behavioral types in the Pi-calculus[C]//Lecture Notes in Computer Science， vol 5210. 2008:372-386.

[9]HU H Y， LV J.Study on behavioral compatibility of components in software architecture using object-oriented paradigm[J]. Journal of Software， 2006， 17(6):1276-1286.

[10]ZHANG W T， PENG Y. Interface compatibility and composition of session-oriented e-service[J]. Chinese Journal of Computers， 2006， 29(7):1047-1056.

[11]辜希武，盧正鼎. 基于Pi演算的BPEL4 WS Web服務組合形式化模型[J]. 計算機科學，2007，34(3):69-74.