李文翔,潘孝銘

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

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

李文翔,潘孝銘

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

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

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

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

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

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

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

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

整個(gè)模型可以描述如下:

根據(jù)π-演算的推理規(guī)則,模型存在著一條路徑從用戶A發(fā)送郵件給服務(wù)器mailer;然后,再由mailer轉(zhuǎn)發(fā)給用戶B.即〈‘iAM〉〈t〉〈t〉〈‘rMB〉.用MWB工具對(duì)上述描述進(jìn)行調(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的驗(yàn)證結(jié)果表明:用戶A在向服務(wù)器M發(fā)送郵件之前做了一些準(zhǔn)備工作‘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在接收到郵件之后,進(jìn)行了‘rMB動(dòng)作,用來(lái)表示接收郵件的后繼動(dòng)作.因此,整個(gè)模型滿足了Email系統(tǒng)的基本功能,即A向B發(fā)送郵件.

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

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

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

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

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

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

3 結(jié)束語(yǔ)

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

[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é)基金資助項(xiàng)目(A 0810013);華僑大學(xué)科研基金資助項(xiàng)目(04BS313)