UTP semantics for web services

Abstract

Web services are increasingly being applied in solving many universal interoperability problems. Business Process Execution Language (BPEL) is a de facto standard for specifying the behaviour of business process. It contains several interesting features, including scope-based compensation, fault handling and shared label synchronisation. This paper presents a design-based formalism for specifying the behaviour of Web services, and provides new healthiness conditions to capture these new programming features. The new models for handling fault and compensation are built as conservative extension of the standard relational model in the sense that the algebraic laws presented in [14] remain valid. The paper also discusses the links between the new model with the design model, and shows that programs can be transformed to the normal forms within the algebraic framework. © Springer-Verlag Berlin Heidelberg 2007.