Verifying BPEL-Like Programs with Hoare Logic
- 1 June 2008
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 151-158
- https://doi.org/10.1109/tase.2008.41
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.Keywords
This publication has 6 references indexed in Scilit:
- Algebraic Approach to Linking the Semantics of Web ServicesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2007
- Towards the theoretical foundation of choreographyPublished by Association for Computing Machinery (ACM) ,2007
- A model for BPEL-like languagesFrontiers of Computer Science in China, 2007
- Analysis of interacting BPEL web servicesPublished by Association for Computing Machinery (ACM) ,2004
- Semantics based verification and synthesis of BPEL4WS abstract processesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- The rely-guarantee method for verifying shared variable concurrent programsFormal Aspects of Computing, 1997