文档介绍：基于多元Pi-演算的Web服务形式化描述模型及其验证
第28卷第8期
2011年8月
计算机应用研究
ApplicationResearchofComputers
基于多元Pi一演算的Web服务形式化
描述模型及其验证木
胡静,冯志勇
(天津大学计算机科学与技术学院,天津300072)
摘要:Web服务组合在运行时多发生由于类型不匹配而产生的错误,为了有效地避免这种错误,在多元Pi一演
,语法定义和判定规则说明单个Web服务的
类型良好性,通过操作语义说明Web服务发生组合时的类型良好性;给出Web服务可替换性定义,并在此定义
,准确说明了Web服
务组合运行时的类型良好性,,提出的定义和判断方法
的有效性.
关键词:Web服务;Web服务组合功能验证;类型化的形式化描述模型;多元Pi一演算
中图分类号:TP301文献标志码:A文章编号:1001—3695(2011)o8—2999-05
—
PolyadicPi—calculusbasedformaldescriptionand
verificationmodelforWebservices
HUJing,FENGZhi?yong
(SchoolofComputerScience&Technology,TianfinUniversity,Tianjin300072,China)
Abstract:|rvpemismatchiSacommonerroratWebservicecompositionrun—time,SOaWebservicefonnaldescriptionmodel
basedonpolyadicPi—
—
sition,andthereplaceabilityofWebservicewasdefinedtoexplainhowthefunctionofWebservicecompositionwasverifled.
ThetypedformaldescriptionmodelproposedaccuratelyexplmnedtheinexistenceoftypeerrorinWebservicecompositionrun—
definitionandmethodproposedabove.
Keywords:Webservice;Webservicecompositionfunctionverification;typedformaldescriptionmodel;polyadicPi—calculus
0引言
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);应用基础及前沿技术
研究计划资助项目(08JCZDJC19800)
作者简介:胡静(1980一),女,河北保定人,讲师,硕士,主要研究方