基于多元Pi-演算的Web服务形式化描述模型及其验证  

Polyadic Pi-calculus based formal description and verification model for Web services

作　　者：胡静[1] 冯志勇[1] 

机构地区：[1]天津大学计算机科学与技术学院,天津300072

出　　处：《计算机应用研究》2011年第8期2999-3003,共5页Application Research of Computers

基　　金：天津市科技支撑计划重点资助项目(08ZCKFGX00700);应用基础及前沿技术研究计划资助项目(08JCZDJC19800)

摘　　要：Web服务组合在运行时多发生由于类型不匹配而产生的错误,为了有效地避免这种错误,在多元Pi-演算的基础上提出了Web服务形式化描述模型。通过基本类型定义、语法定义和判定规则说明单个Web服务的类型良好性,通过操作语义说明Web服务发生组合时的类型良好性;给出Web服务可替换性定义,并在此定义基础上说明如何进行Web服务组合的功能验证。提出的类型化Web服务形式化描述模型,准确说明了Web服务组合运行时的类型良好性,以及Web服务组合的功能验证方法。最后通过例子说明,提出的定义和判断方法的有效性。Type mismatch is a common error at Web service composition run-time,so a Web service formal description model based on polyadic Pi-calculus was built to avoid the error.The definition of basic type,grammar and verification rules were used to show the type goodness of single Web service,the operational semantics was used to show the type goodness of composition,and the replaceability of Web service was defined to explain how the function of Web service composition was verified.The typed formal description model proposed accurately explained the inexistence of type error in Web service composition run-time and the verification method of Web service composition.Finally,the example instructed that the effectiveness of all the definition and method proposed above.

关 键 词：WEB服务 Web服务组合功能验证 类型化的形式化描述模型 多元Pi-演算 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]