摘要
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.
出处
《微计算机信息》
2010年第30期209-211,共3页
Control & Automation
关键词
PI演算
WEB服务
服务组合
组合验证
π-Calculus
Web Service
Service Composition
Composition Verification
