TY - GEN
T1 - Animating the approach of deriving operational semantics from algebraic semantics for web services
AU - Wang, Qian
AU - Zhu, Huibiao
PY - 2011
Y1 - 2011
N2 - Web services have became 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 already explored the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models respectively. Meanwhile, we have also explored the link between the operational semantics and algebraic semantics for BPEL. Our approach was to derive the operational semantics from algebraic semantics. This paper considers the animation approach for the link between operational semantics and algebraic semantics for BPEL. The Logic Programming Language Prolog is applied to support for the development [2]. Firstly we animate the operational semantics for BPEL. Our approach for deriving operational semantics from algebraic semantics proceeds through head normal form. Secondly, we animate the algebraic laws for BPEL. Based on this, we animate the generation of head normal form for each program. Four typical forms are introduced for defining head normal form. Thirdly, we explore the animation for deriving operational semantics from head normal form. From various test results, the first and third exploration show that the soundness and completeness for the operational semantics from the algebraic semantics for BPEL.
AB - Web services have became 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 already explored the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models respectively. Meanwhile, we have also explored the link between the operational semantics and algebraic semantics for BPEL. Our approach was to derive the operational semantics from algebraic semantics. This paper considers the animation approach for the link between operational semantics and algebraic semantics for BPEL. The Logic Programming Language Prolog is applied to support for the development [2]. Firstly we animate the operational semantics for BPEL. Our approach for deriving operational semantics from algebraic semantics proceeds through head normal form. Secondly, we animate the algebraic laws for BPEL. Based on this, we animate the generation of head normal form for each program. Four typical forms are introduced for defining head normal form. Thirdly, we explore the animation for deriving operational semantics from head normal form. From various test results, the first and third exploration show that the soundness and completeness for the operational semantics from the algebraic semantics for BPEL.
UR - https://www.scopus.com/pages/publications/84863048762
U2 - 10.1109/HASE.2011.56
DO - 10.1109/HASE.2011.56
M3 - 会议稿件
AN - SCOPUS:84863048762
SN - 9780769546155
T3 - Proceedings of IEEE International Symposium on High Assurance Systems Engineering
SP - 57
EP - 62
BT - Proceedings - 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, HASE 2011
T2 - 13th IEEE International Symposium on High Assurance Systems Engineering, HASE 2011
Y2 - 10 November 2011 through 12 November 2011
ER -