一种Web服务组合形式化模型及验证方法  

One formal model and verify method of Web services composition

作　　者：周昆[1] 金可音[1] 

机构地区：[1]湖南工业大学计算机与通信学院,湖南株洲412000

出　　处：《微计算机信息》2010年第30期209-211,共3页Control & Automation

摘　　要：Web服务组合研究领域中一个重要的研究内容是服务组合验证问题,通过对Web服务组合建立形式化模型,在服务组合之前进行形式化验证,以确保满足服务组合符合设计者的预期目标。Pi演算是一种适合描述动态拓扑结构的并发系统的进程代数。本文首先介绍了Pi演算的基本语法,建立了Pi演算与BPEL4WS的映射关系,提出了一种基于Pi演算的BPEL4WS的形式化模型,最后通过案例给出了模型的验证过程。One of the most important issues in the Web services composition researching area is how to verify the correctness of Web services composition.This paper proposes a formal model of Web services,which is used to formally verify before the services composition,so,we can be sure that the result of the services composition meet with the designer＇s initial goal.π calculus is fit to describe the dynamic topology architecture of the concurrent system.Firstly,This paper introduce the basic grammar of the π calculus,then,expounds the mapping between π calculus and BPEL4WS,proposes a formal model of BPEL4WS which is based on π calculus,at last,the model verification process is also introduced through a case study.

关 键 词：PI演算 WEB服务 服务组合 组合验证 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]