Verifying BPEL-Like Programs with Hoare Logic

Chenguang Luo, Shengchao Qin, Zongyan Qiu

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

    Abstract

    The WS-BPEL language has become a de facto standard for modeling Web-based business processes. One of its essential features is the fully programmable compensation mechanism. To understand it better, many works have mainly focused on formal semantic models for WS-BPEL. In this paper, we make one step forward by investigating the verification problem for business processes written in BPEL-like languages. We propose a set of proof rules in Hoare-logic style as an axiomatic verification system for a BPEL-like core language containing key features such as data states, fault and compensation handling. We also propose a big-step operational semantics which incorporates all these key features. Our verification rules are proven sound with respect to this underlying semantics. The application of the verification rules is illustrated via the proof search process for a nontrivial example.
    Original languageEnglish
    Title of host publicationSecond IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China
    PublisherIEEE
    ISBN (Print)978-0-7695-3249-3
    DOIs
    Publication statusPublished - 2008
    EventSecond IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering - Nanjing, China
    Duration: 17 Jun 200819 Jun 2008
    Conference number: 2

    Conference

    ConferenceSecond IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering
    Abbreviated titleTASE 2008
    CountryChina
    CityNanjing
    Period17/06/0819/06/08

    Fingerprint Dive into the research topics of 'Verifying BPEL-Like Programs with Hoare Logic'. Together they form a unique fingerprint.

  • Cite this

    Luo, C., Qin, S., & Qiu, Z. (2008). Verifying BPEL-Like Programs with Hoare Logic. In Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China IEEE. https://doi.org/10.1109/TASE.2008.41