Web Services: A Process Algebra Approach

TL;DR

This paper introduces a framework that uses process algebras for designing and verifying Web services, enabling automatic code generation and flexible verification methods.

Contribution

It presents a novel approach linking abstract process algebra specifications with executable Web services, enhancing verification and design flexibility.

Findings

Framework supports automatic BPEL4WS code generation

Process algebra verification tools improve Web service correctness

Hierarchical refinement aids in Web service design

Abstract

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 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. Several choices are available: design and correct errors in BPEL4WS, using process algebra verification tools, or design and correct in process algebra and automatically obtaining the corresponding BPEL4WS code. The approaches can be combined. Process algebra are not useful only for temporal logic verification: we remark the use of simulation/bisimulation both for verification and for the hierarchical refinement design method. It is worth noting that our approach allows the use of any process algebra depending on the needs of the user at different levels (expressiveness, existence of reasoning tools, user expertise).