Email系统特征交互问题的π-演算检测

李文翔,潘孝铭

(华侨大学计算机科学与技术学院,福建泉州 362021)

Email系统特征交互问题的π-演算检测

李文翔,潘孝铭

(华侨大学计算机科学与技术学院,福建泉州 362021)

采用π-演算给出基于客户端-服务器模式的Email系统,以及系统中特征的行为描述;然后,利用μ -演算描述和分析Email系统中存在的特征交互问题.最后,利用移动工作台软件工具,验证基于π-演算描述的移动并发系统.

特征交互;Email系统;π-演算;μ-演算;移动工作台

特征交互问题最早是由美国贝尔通信实验针对电信系统提出的[1].它主要表现为软件系统中可组合的服务或者特征之间的非预期的相互影响,而这些影响会导致系统无法向用户提供正常的服务或者影响服务的质量.2001年10月,Feature Interaction Wo rkshop国际会议上明确地提出了研究电信领域以外的其他软件系统中存在的特征交互问题[2].目前,应用于特征交互问题检测,主要有软件工程方法,形式化方法和在线检测方法3个方法[3-4].形式化方法主要在需求规约阶段对基础子系统和特征进行描述,然后分析和检测特征之间的交互问题.M ilner等[5-6]提出以进程间的移动通信为研究重点的并发理论——π-演算.其主要优点是可以用一个动态通信结构来表示系统,不仅可以传递变量和值等,也可以传递通道名,且将这些实体统称为名字而不作区分.μ-演算[7]是 HML(Hennessy-M ilner Logic)逻辑的扩展.它增加了最大不动点和最小不动点的概念,比HML具有更强的表达能力,可以处理无限状态的进程.本文采用π-演算对Email模型进行行为描述,利用μ-演算对特征交互进行描述分析和检测.

1 Email系统模型的π-演算描述

图1为Email系统模型.它包含了一系列的用户(Client)和一个服务器(M ailer).用户和服务器之间的通信是异步进行的.每个用户都有一个唯一的地址来标识自己,用户可以发送和接收邮件;服务器可以将邮件发送给用户.

图1 Email系统模型Fig.1 Email system model

用户i有两个通信通道:输出动作network和输入动作mailbox.前者用于用户i向服务器发送邮件,后者用于用户i接收来自服务器的邮件,即用户i的收件箱.在发送邮件前,用户i有一个输出动作iM,表示发送前的准备工作.接收到邮件后,用户i执行输出动作rM,表示接收后的用户i的一些后续操作.采用基于 New Jersey SML语言编辑器的移动工作台(Mobility Wo rkbench,MWB)工具[8-9],分析和验证基于π-演算描述的移动并发系统.用户A的π-演算描述如下:其中:agnentA和agentB分别表示用户A和用户B的地址;msg表示所传递的邮件;mailer在整个模型中只起到分发邮件的作用,它拥有一个network输入动作,用于接收来自用户的邮件,以及与多个用户进行通信的通道mailbox1,mailbox2,…,mailboxn.这里,考虑2个用户之间的邮件传递.因此,mailer在MWB中的π-演算描述如下:

整个模型可以描述如下:

根据π-演算的推理规则,模型存在着一条路径从用户A发送邮件给服务器mailer;然后,再由mailer转发给用户B.即〈‘iAM〉〈t〉〈t〉〈‘rMB〉.用MWB工具对上述描述进行调试,证明了M ail (iAM,iBM,rM A,rMB)|=〈‘iAM〉〈t〉〈t〉〈‘rMB〉TT.

Email系统模型中,M ail〈iAM,iBM,rM A,rMB〉|=〈‘iAM〉〈t〉〈t〉〈‘rMB〉TT的验证结果表明:用户A在向服务器M发送邮件之前做了一些准备工作‘iAM,接着发送邮件到服务器,即A→M:{m sg, agentA,agentB};服务器M在接收到邮件之后,根据A提供的目标接收者B,将邮件转发给用户B,即M→B:{m sg,agentA,agentB};用户B在接收到邮件之后,进行了‘rMB动作,用来表示接收邮件的后继动作.因此,整个模型满足了Email系统的基本功能,即A向B发送邮件.

2 Email系统的特征交互分析

文献[4]给出了Email系统中所有的特征.此处,只考虑一个最基本的特征,即自动回复.用户申请自动回复服务后,一旦用户接收到邮件,就会自动发送一封邮件回复给定发送方.因此,在上述的模型描述中,在用户mailbox动作后面添加一个输出动作network.考虑到后面问题描述的方便,将这个输出动作添加到输出动作r之后.一个client的MWB中π-演算的描述如下:

当都定制了自动回复功能的用户A和B进行邮件传递的时候,模型中就存在着特征交互.即当用户B接收来自用户A的邮件后,就自动发送了回复邮件;而A收到邮件后,A也向B发送回复邮件,B收到邮件后再次向A发送回复邮件.

如此往复,A和B之间就存在着一条循环路径,且此循环是无条件的.因此,在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中的验证结果表明:在用户B确认接收到来自用户A发出的邮件时,B在动作‘rMB之后做了一个自动回复动作,即B→M:{m sg,agentB,agentA};服务器M在接收到这个回复邮件时,根据B提供的邮件接收者将邮件通过通道mailboxA将邮件转发给用户A.此时,在用户A确认接收到邮件时,由于自动回复功能,A发送了回复邮件;而服务器M又将回复邮件转发给B.

如此往复,用户A、服务器M和用户B这3者之间就陷入了不断发送和转发回复邮件的无限循环步骤,则系统就发生了自动回复特征交互问题.

3 结束语

对于Email系统的所有特征,只对自动回复特征进行了描述和分析.对于消息过滤和自动回复等其他的特征交互问题,未作描述和分析.同时,在研究过程中,出现了状态空间爆炸的问题,这也是进一步要解决的问题.

[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.

(责任编辑:陈志贤英文审校:吴逢铁)

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-),男,副教授,主要从事形式化技术的研究.E-mail:panxiaom@hqu.edu.cn.

福建省自然科学基金资助项目(A 0810013);华侨大学科研基金资助项目(04BS313)