TY - GEN
T1 - Linking algebraic semantics and operational semantics for web services using maude
AU - Liu, Peng
AU - Zhu, Huibiao
AU - Qin, Shengchao
AU - Brooke, Phillip J.
AU - Wu, Xi
PY - 2013
Y1 - 2013
N2 - Web services have become more and more important in these years. It is of key importance for enterprise web applications to combine different services available to accomplish complex business processes. BPEL4WS (BPEL) is the OASIS standard for web services composition and orchestration. It contains several distinct features, including scope-based compensation and fault handling mechanism. We have already studied the semantics for BPEL, including the operational semantics, algebraic semantics and their linking theory. This paper considers the mechanical approach to linking the algebraic semantics and operational semantics for BPEL. Our approach is to generate operational semantics from algebraic semantics, and to use equational and rewriting logic system Maude to mechanize the linking between the two semantics. Firstly, we investigate the algebraic laws in the Maude approach. Based on the algebraic semantics, the generation of head normal form is explored. Secondly, we consider the Maude approach to deriving the operational semantics from algebraic semantics, where the derivation strategy is based on the concept of head normal form. Our mechanical approach using Maude can visually show the head normal form of each program, as well as the execution steps of a program based on the derivation strategy.
AB - Web services have become more and more important in these years. It is of key importance for enterprise web applications to combine different services available to accomplish complex business processes. BPEL4WS (BPEL) is the OASIS standard for web services composition and orchestration. It contains several distinct features, including scope-based compensation and fault handling mechanism. We have already studied the semantics for BPEL, including the operational semantics, algebraic semantics and their linking theory. This paper considers the mechanical approach to linking the algebraic semantics and operational semantics for BPEL. Our approach is to generate operational semantics from algebraic semantics, and to use equational and rewriting logic system Maude to mechanize the linking between the two semantics. Firstly, we investigate the algebraic laws in the Maude approach. Based on the algebraic semantics, the generation of head normal form is explored. Secondly, we consider the Maude approach to deriving the operational semantics from algebraic semantics, where the derivation strategy is based on the concept of head normal form. Our mechanical approach using Maude can visually show the head normal form of each program, as well as the execution steps of a program based on the derivation strategy.
UR - https://www.scopus.com/pages/publications/84885232268
U2 - 10.1109/ICECCS.2013.46
DO - 10.1109/ICECCS.2013.46
M3 - 会议稿件
AN - SCOPUS:84885232268
SN - 9780769550077
T3 - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
SP - 260
EP - 263
BT - Proceedings - 2013 International Conference on Engineering of Complex Computer Systems, ICECCS 2013
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013
Y2 - 17 July 2013 through 19 July 2013
ER -