Linking the Semantics of BPEL Using Maude

Peng Liu, Huibiao Zhu, Shengchao Qin, Phillip J. Brooke, Xi Wu

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    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 process. 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 operational semantics and algebraic 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. Finally, we also mechanize the derived operational semantics. The results mechanized from the second and third exploration indicate that the transition system of the derived operational semantics is the same as the one based on the derivation strategy.
    Original languageEnglish
    Title of host publication 2013 20th Asia-Pacific Software Engineering Conference (APSEC)
    ISBN (Electronic)9781479921447
    Publication statusPublished - 2013
    Event20th Asia-Pacific Software Engineering Conference - Bangkok, Thailand
    Duration: 2 Dec 20135 Dec 2013
    Conference number: 20


    Conference20th Asia-Pacific Software Engineering Conference
    Abbreviated titleAPSEC 2013


    Dive into the research topics of 'Linking the Semantics of BPEL Using Maude'. Together they form a unique fingerprint.

    Cite this