The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs

Huibiao Zhu, Qiwen Xu, Chris Ma, Shengchao Qin, Zongyan Qiu

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

    Abstract

    Web services have become more and more important in these years, and 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. This paper focuses on the verification of BPEL programs, especially the verification of concurrent BPEL programs. The rely/guarantee approach is applied. Firstly, we present the operational semantics for BPEL programs. Secondly we apply the rely/guarantee method in the design of the verification rules. The rules can handle the features of BPEL programs, including compensation, fault handling and concurrency. Finally, the whole proof system is proved to be sound based on our operational semantics.
    Original languageEnglish
    Title of host publication Software Engineering and Formal Methods. SEFM 2012
    EditorsG. Eleftherakis , M Hinchey , M Holcombe
    PublisherSpringer Berlin
    ISBN (Electronic)9783642338267
    ISBN (Print)9783642338250
    DOIs
    Publication statusPublished - 2012
    EventSoftware Engineering and Formal Methods - 10th International Conference - Thessaloniki, Greece
    Duration: 1 Oct 20125 Oct 2012
    Conference number: 10

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer, Berlin
    Volume7504

    Conference

    ConferenceSoftware Engineering and Formal Methods - 10th International Conference
    Abbreviated titleSEFM 2012
    CountryGreece
    CityThessaloniki
    Period1/10/125/10/12

    Fingerprint Dive into the research topics of 'The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs'. Together they form a unique fingerprint.

  • Cite this

    Zhu, H., Xu, Q., Ma, C., Qin, S., & Qiu, Z. (2012). The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs. In G. Eleftherakis , M. Hinchey , & M. Holcombe (Eds.), Software Engineering and Formal Methods. SEFM 2012 (Lecture Notes in Computer Science; Vol. 7504). Springer Berlin. https://doi.org/10.1007/978-3-642-33826-7_12