Animating The Linking Of BPEL Semantics

As SOA (Service-Oriented Architecture) is wide applied in industry field in recent years, web services and other web-based applications have attracted much attention. BPEL (Business Process Execution Language), as one of the most important web-based business process languages, have been becoming more and more important. In order to correctly develop service-oriented information system, the precise understanding of BPEL is the precondition.BPEL contains several interesting features, such as the scope-based compensation and fault handling mechanism and so on. Zhu et.al. have already explored the operational semantics and algebraic semantics for BPEL. Furthermore, they have also developed the concept of head normal form, a set of algebraic laws, as well as the derivation of operational semantics from algebraic semantics. All of these work have proved the correctness of the operational semantics from a theoretical point of view.This paper animates the link between operational semantics and algebraic semantics for BPEL via the emulator implemented by logic programming language Prolog and Maude respectively. We firstly consider the animation of operational semantics for BPEL. The various test results make sure the correctness of operational semantics. Secondly we animate various algebraic laws for scope and parallel composition. On this basis, we define the generation of head normal form for every program with the help of algebraic laws. At last the derivation strategy for developing operational semantics from algebraic semantics is implemented. From a variety of simulation results, the equivalence between the operational semantics and the derivation of operational semantics from algebraic semantics could be proved from the perspective of practice. Meanwhile, the animation approach also provides a reference for the proof of semantics link for other web-based languages in the future.