Algebraic Approach to Linking the Semantics of Web Services
- 1 September 2007
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 315-328
- https://doi.org/10.1109/sefm.2007.4
Abstract
Web services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the Web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault handling mechanism. We have considered the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models respectively. In this paper, we consider the inverse work, deriving the operational semantics and denotational semantics from algebraic semantics for BPEL. In our model, we introduce four types of typical programs, by which every program can be expressed as the summation of these four types. Based on the algebraic semantics, the strategy for deriving the operational semantics is provided and a transition system is derived by strict proof. This can be considered as the soundness exploration for the operational semantics based on the algebraic semantics. Further, the equivalence between the derivation strategy and the derived transition system is explored, which can be considered as the completeness of the operational semantics. Finally, the derivation of the denotational semantics from algebraic semantics is explored, which can support to reason about more program properties easily.Keywords
This publication has 10 references indexed in Scilit:
- Looking into Compensable TransactionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2007
- An Operational Approach to BPEL-like ProgrammingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2007
- A model for BPEL-like languagesFrontiers of Computer Science in China, 2007
- Towards the Semantics and Verification of BPEL4WSElectronic Notes in Theoretical Computer Science, 2006
- Semantics of BPEL4WS-Like Fault and Compensation HandlingPublished by Springer Nature ,2005
- Temporal Verification of Reactive SystemsPublished by Springer Nature ,1995
- Specification and Proof in Real Time CSPPublished by Cambridge University Press (CUP) ,1993
- The Temporal Logic of Reactive and Concurrent SystemsPublished by Springer Nature ,1992
- Laws of programmingCommunications of the ACM, 1987
- SagasPublished by Association for Computing Machinery (ACM) ,1987