基于多元Pi-演算的Web服务形式化描述模型及其验证第28卷第8期2011年8月计算机应用研究ApplicationResearchofComputers基于多元Pi一演算的Web服务形式化描述模型及其验证木胡静,冯志勇(天津大学计算机科学与技术学院,天津300072)摘要:Web服务组合在运行时多发生由于类型不匹配而产生的错误,为了有效地避免这种错误,在多元Pi一演算的基础上提出了Web服务形式化描述模型.通过基本类型定义,语法定义和判定规则说明单个Web服务的类型良好性,通过操作语义说明Web服务发生组合时的类型良好性;给出Web服务可替换性定义,并在此定义基础上说明如何进行Web服务组合的功能验证.提出的类型化Web服务形式化描述模型,准确说明了Web服务组合运行时的类型良好性,以及Web服务组合的功能验证方法.最后通过例子说明,提出的定义和判断方法的有效性.关键词:Web服务;Web服务组合功能验证;类型化的形式化描述模型;多元Pi一演算:TP301文献标志码:A:1001—3695(2011)o8—2999-05—PolyadicPi—calculusbasedformaldescriptionandverificationmodelforWebservicesHU激ng,FENGZhi?yong(SchoolofComputerScienceTechnology,TianfinUniversity,Tian激n300072,China)Abstract:|rvpemismatchiSacommonerroratWebservicecompositionrun—time,SOaWebservicefonnaldescriptionmodelbasedonpolyadicPi——sition,andthereplaceabilityofWebservicewasdefinedtoexplainhowthefunctionofWebservicecompositionwasverifled.ThetypedformaldescriptionmodelproposedaccuratelyexplmnedtheinexistenceoftypeerrorinWebservicecompositionrun—definitionandmethodproposedabove.Keywords:Webservice;Webservicecompositionfunctionverification;typedformaldescriptionmodel;polyadicPi—calculus0引言web服务组合的不良性除了由于发生交互时行为的不匹配导致的死锁等现象之外,数据类型的不一致性也是发生错误的重要因素.为了判断类型是否匹配,需要在原形式化描述模型的基础上加人类型系统,增加变量和信道类型,并给出了其改写,除了正确约简之外,加入了由于类型不匹配造成的交互了检查Web服务组合是否存在着各种原因引起的死锁,Web服务组合功能的验证是为了检查组合的Web服务是否能够满足用户的需求.无论用什么办法对Web服务组合建模后,形式化的模型总是可以方便地找到对Web服务组合进行行为验环境不同有不同的要求.1研究现状类型系统是一种根据所计算出值的种类对词语进行分类,入了简单的类型系统从而扩充到多元Pi一演算(一个通道可以传送名字元组),提出了通道分类的概念(sorting),这样多元一演的基础上对通道作了进一步的分类,Sangiorgi等人也在多元一演算的基础上定义了一个简单的类型系统SimplyTypedPi.calculus,用于描述并发系统的行为和数据类型的一致性.当前,基于一演算的Web服务组合形式化验证的工作主义的进程弱等价性质定义Web服务组合的相容性J,并通过相容性来验证web服务组合的运行过程和功能;或者是直接利用一演算的自动验证工具MWB,通过对Web服务组合弱等价性的自动验证,来完成对Web服务组合的行为验证和功能验证;或者基于类型化的Pi一演算对Web服务组合进行收稿日期:2011—01—22;修回日期:20ll一02—28基金项目:天津市科技支撑计划重点资助项目(08ZCKFGX00700);应用基础及前沿技术研究计划资助项目(08JC政法JC19800)作者简介:胡静(1980一),女,河北保定人,讲师,硕士,主要研究方向为SOA,形式化描述,Pi-演算(mavis_huhu@tju.edu);冯志勇(1964一),男,教授,博导,主要研究方向为软件体系结构,知识工程,语义网,multi—agent系统等.?30oO?计算机应用研究第28卷形式化建模和相容性分析.Web相容性主要应用于当发生组合的Web子服务不可用时,通过判断替换的Web子服务和原Web子服务的交互环境同时不可用需要寻找替换时,就无法使用相容性来进行判断.2类型化的Web服务形式化描述模型定义1类型假设.给名字a指定类型,称为类型假设,记为Ⅱ:To设集,通常记为,和△.对于类型假设集中的每个名字,只能有一个类型与其对应,即F::={a:f∈N,i≠≠ai},类型假设集,中包含的所有的名字记为supp(F).定义3类型假设集的合并.用,,△来表示类型假...