李文翔,潘孝銘

(華僑大學(xué)計算機科學(xué)與技術(shù)學(xué)院,福建泉州 362021)

Email系統(tǒng)特征交互問題的π-演算檢測

李文翔,潘孝銘

(華僑大學(xué)計算機科學(xué)與技術(shù)學(xué)院,福建泉州 362021)

采用π-演算給出基于客戶端-服務(wù)器模式的Email系統(tǒng),以及系統(tǒng)中特征的行為描述;然后,利用μ -演算描述和分析Email系統(tǒng)中存在的特征交互問題.最后,利用移動工作臺軟件工具,驗證基于π-演算描述的移動并發(fā)系統(tǒng).

特征交互;Email系統(tǒng);π-演算;μ-演算;移動工作臺

特征交互問題最早是由美國貝爾通信實驗針對電信系統(tǒng)提出的[1].它主要表現(xiàn)為軟件系統(tǒng)中可組合的服務(wù)或者特征之間的非預(yù)期的相互影響,而這些影響會導(dǎo)致系統(tǒng)無法向用戶提供正常的服務(wù)或者影響服務(wù)的質(zhì)量.2001年10月,Feature Interaction Wo rkshop國際會議上明確地提出了研究電信領(lǐng)域以外的其他軟件系統(tǒng)中存在的特征交互問題[2].目前,應(yīng)用于特征交互問題檢測,主要有軟件工程方法,形式化方法和在線檢測方法3個方法[3-4].形式化方法主要在需求規(guī)約階段對基礎(chǔ)子系統(tǒng)和特征進行描述,然后分析和檢測特征之間的交互問題.M ilner等[5-6]提出以進程間的移動通信為研究重點的并發(fā)理論——π-演算.其主要優(yōu)點是可以用一個動態(tài)通信結(jié)構(gòu)來表示系統(tǒng),不僅可以傳遞變量和值等,也可以傳遞通道名,且將這些實體統(tǒng)稱為名字而不作區(qū)分.μ-演算[7]是 HML(Hennessy-M ilner Logic)邏輯的擴展.它增加了最大不動點和最小不動點的概念,比HML具有更強的表達能力,可以處理無限狀態(tài)的進程.本文采用π-演算對Email模型進行行為描述,利用μ-演算對特征交互進行描述分析和檢測.

1 Email系統(tǒng)模型的π-演算描述

圖1為Email系統(tǒng)模型.它包含了一系列的用戶(Client)和一個服務(wù)器(M ailer).用戶和服務(wù)器之間的通信是異步進行的.每個用戶都有一個唯一的地址來標(biāo)識自己,用戶可以發(fā)送和接收郵件;服務(wù)器可以將郵件發(fā)送給用戶.

圖1 Email系統(tǒng)模型Fig.1 Email system model

用戶i有兩個通信通道:輸出動作network和輸入動作mailbox.前者用于用戶i向服務(wù)器發(fā)送郵件,后者用于用戶i接收來自服務(wù)器的郵件,即用戶i的收件箱.在發(fā)送郵件前,用戶i有一個輸出動作iM,表示發(fā)送前的準備工作.接收到郵件后,用戶i執(zhí)行輸出動作rM,表示接收后的用戶i的一些后續(xù)操作.采用基于 New Jersey SML語言編輯器的移動工作臺(Mobility Wo rkbench,MWB)工具[8-9],分析和驗證基于π-演算描述的移動并發(fā)系統(tǒng).用戶A的π-演算描述如下:其中:agnentA和agentB分別表示用戶A和用戶B的地址;msg表示所傳遞的郵件;mailer在整個模型中只起到分發(fā)郵件的作用,它擁有一個network輸入動作,用于接收來自用戶的郵件,以及與多個用戶進行通信的通道m(xù)ailbox1,mailbox2,…,mailboxn.這里,考慮2個用戶之間的郵件傳遞.因此,mailer在MWB中的π-演算描述如下:

整個模型可以描述如下:

根據(jù)π-演算的推理規(guī)則,模型存在著一條路徑從用戶A發(fā)送郵件給服務(wù)器mailer;然后,再由mailer轉(zhuǎn)發(fā)給用戶B.即〈‘iAM〉〈t〉〈t〉〈‘rMB〉.用MWB工具對上述描述進行調(diào)試,證明了M ail (iAM,iBM,rM A,rMB)|=〈‘iAM〉〈t〉〈t〉〈‘rMB〉TT.

Email系統(tǒng)模型中,M ail〈iAM,iBM,rM A,rMB〉|=〈‘iAM〉〈t〉〈t〉〈‘rMB〉TT的驗證結(jié)果表明:用戶A在向服務(wù)器M發(fā)送郵件之前做了一些準備工作‘iAM,接著發(fā)送郵件到服務(wù)器,即A→M:{m sg, agentA,agentB};服務(wù)器M在接收到郵件之后,根據(jù)A提供的目標(biāo)接收者B,將郵件轉(zhuǎn)發(fā)給用戶B,即M→B:{m sg,agentA,agentB};用戶B在接收到郵件之后,進行了‘rMB動作,用來表示接收郵件的后繼動作.因此,整個模型滿足了Email系統(tǒng)的基本功能,即A向B發(fā)送郵件.

2 Email系統(tǒng)的特征交互分析

文獻[4]給出了Email系統(tǒng)中所有的特征.此處,只考慮一個最基本的特征,即自動回復(fù).用戶申請自動回復(fù)服務(wù)后,一旦用戶接收到郵件,就會自動發(fā)送一封郵件回復(fù)給定發(fā)送方.因此,在上述的模型描述中,在用戶mailbox動作后面添加一個輸出動作network.考慮到后面問題描述的方便,將這個輸出動作添加到輸出動作r之后.一個client的MWB中π-演算的描述如下:

當(dāng)都定制了自動回復(fù)功能的用戶A和B進行郵件傳遞的時候,模型中就存在著特征交互.即當(dāng)用戶B接收來自用戶A的郵件后,就自動發(fā)送了回復(fù)郵件;而A收到郵件后,A也向B發(fā)送回復(fù)郵件,B收到郵件后再次向A發(fā)送回復(fù)郵件.

如此往復(fù),A和B之間就存在著一條循環(huán)路徑,且此循環(huán)是無條件的.因此,在MWB中以這樣的公式表示:〈‘iAM〉〈t〉〈t〉〈‘rMB〉(nuZ.(〈t〉〈t〉〈‘rMA〉〈t〉〈t〉〈‘rMB〉Z)).然后,利用check命令驗證模型M ail是否滿足上述公式.若是,則模型中存在著特征交互.

M ail〈iAM,iBM,rMA,rMB〉|=〈‘iAM〉〈t〉〈t〉〈‘rMB〉(nuZ.(〈t〉〈t〉〈‘rMA〉〈t〉〈t〉〈‘rMB〉Z))在MWB中的驗證結(jié)果表明:在用戶B確認接收到來自用戶A發(fā)出的郵件時,B在動作‘rMB之后做了一個自動回復(fù)動作,即B→M:{m sg,agentB,agentA};服務(wù)器M在接收到這個回復(fù)郵件時,根據(jù)B提供的郵件接收者將郵件通過通道m(xù)ailboxA將郵件轉(zhuǎn)發(fā)給用戶A.此時,在用戶A確認接收到郵件時,由于自動回復(fù)功能,A發(fā)送了回復(fù)郵件;而服務(wù)器M又將回復(fù)郵件轉(zhuǎn)發(fā)給B.

如此往復(fù),用戶A、服務(wù)器M和用戶B這3者之間就陷入了不斷發(fā)送和轉(zhuǎn)發(fā)回復(fù)郵件的無限循環(huán)步驟,則系統(tǒng)就發(fā)生了自動回復(fù)特征交互問題.

3 結(jié)束語

對于Email系統(tǒng)的所有特征,只對自動回復(fù)特征進行了描述和分析.對于消息過濾和自動回復(fù)等其他的特征交互問題,未作描述和分析.同時,在研究過程中,出現(xiàn)了狀態(tài)空間爆炸的問題,這也是進一步要解決的問題.

[1]CAM ERON J E,GRIFFETH N,L IN Y J,et al.A feature interaction benchmark for IN and beyond[J].IEEECommunications Magazine,1993,31(3):64-69.

[2]PULVERMUELLER E,SPECK A,COPL IEN J,et al.Feature interaction in composed system s[C]∥Proceedingsof the Workshopson Object-Oriented Technology.London:Sp ringer-Verlag,2001:86-97.

[3]KIMBLER K,BOUMA L G.Feature interactions in telecommunications and software systems(Ⅴ)[M].Amsterdam:IOS Press,1998.

[4]CALDER N,MAGILL E.Feature interactions in telecommunications and software system s(Ⅵ)[M].Am sterdam: IOS Press,2000.

[5]M ILNER R.Communicating and mobile systems:Theπ-calculus[M].Cambridge:Cambridge University Press, 1999.

[6]M ILNER R.The polyadicπ-calculus:A tuto rial[C]∥BAUER F,et al.Logic and A lgebra of Specification.Berlin: Sp ringer-Verlag,1992:203-246.

[7]BRADFIELD J,STIRL ING C.Modalμ-calculi[C]∥BLACKBURN P,et al.The Handbook of Modal Logic.New Yo rk:Elsevier Science L td,2006:721-756.

[8]V ICTOR B.The mobility wo rkbench user′s guide:Polyadic version 3.122[R].Uppsala:Uppsala University,1995.

[9]V ICTOR B.A verification tool for the polyadicπ-calculus[R].Uppsala:Uppsala University,1994.

(責(zé)任編輯:陳志賢英文審校:吳逢鐵)

Detection of Feature In teractions in Email System Based onπ-Calculus

L IWen-xiang,PAN Xiao-ming
(College of Computer Science and Technologe,Huaqiao University,Quanzhou 362021,China)

In this paper,the email system based on client-server and the features are defined in a behavio ral descrip tion by usingπ-calculus.Then we useμ-calculus to describe and analyze the feature interactions problem s in this system. And at last we use a tool called mobility wo rkbench to prove themobile concurrent system described byπ-calculus.

feature interactions;Email system;π-calculus;μ-calculus;mobility wo rkbench

TP 311.5

A

1000-5013(2011)02-0175-03

2009-10-21

潘孝銘(1968-),男,副教授,主要從事形式化技術(shù)的研究.E-mail:panxiaom@hqu.edu.cn.

福建省自然科學(xué)基金資助項目(A 0810013);華僑大學(xué)科研基金資助項目(04BS313)