Describing and reasoning on Web Services using process algebra

We argue that essential facets of Web Services (WSs), and especially, those useful to understand their interaction, are best described using process-algebraic notations. WS description and execution languages such as BPEL are essentially process description languages; they are based on primitives for behaviour description and message exchange, which can also be found in more abstract languages such as Process Algebras (PAs). One legitimate question is therefore whether the WSs community can benefit from the sophisticated languages and tools developed in the PA area. Our investigations suggest a positive answer and we claim that PAs provide solutions to a number of challenges raised by the WSs paradigm, among which are central issues of orchestration and choreography. We show on a case study that readily available tools based on PA are effective at verifying that compositions of services obtained by choreography and orchestration conform their requirements and respect properties. We suggest a general framework based on a mapping between PA and WSs written in BPEL, and illustrate both the modelling of services by PA and the use of reasoning tools. Copyright © 2006 Inderscience Enterprises Ltd.