A Pi-calculus Based Formal Model for BPEL4 WS Web Service Composition
Gu Xi · 2007
One of important issue in Web service composition researching area is how to describe Web service composition formally and verify the correctness of Web service composition. A formal model of Web service composition can be used to check and verify Web service composition so that the correctness of Web service composition can be guaranteed. Pi-calculus is a kind of process algebra which is suitable for modeling Web service composition. This paper introduces basic syntax of Pi-calculus. For the most important kind of specification of specifying and executing workflow based Web service composition- Business Process Execution Language for Web Services(BPEL4WS), the paper defines the conception mapping between Pi-calculus and BPEL4WS and presents a Pi-calculus based formal model for BPEL4WS.The model verification method is also introduced through a case study.