Web Services: A Process Algebra Approach

It is now well-admitted that formal methods are helpful for many issues raised in the Web service area. In this paper we present a framework for the design and the verification of WSs using process algebras and their tools. We define a two-way mapping between abstract specifications written using these calculi and executable Web services written in BPEL4WS; the translation includes also compensation, event, and fault handlers. The following choices are available: design and verification in BPEL4WS, using process algebra tools, or design and verification in process algebra and automatically obtaining the corresponding BPEL4WS code. The approaches can be combined. Process algebras are not useful only for temporal logicverification: we remark the use of simulation/bisimulation for verification, for the hierarchical refinement design method, for the service redundancy analysis in a community, and for replacing a service withanother one in a composition.