We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

Verifying BPEL-like programs with Hoare logic.

Luo, C. and Qin, S. and Qiu, Z. (2008) 'Verifying BPEL-like programs with Hoare logic.', Frontiers of computer science in China., 2 (4). pp. 344-356.


The WS-BPEL language has recently 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 recent 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.

Item Type:Article
Keywords:WS-BPEL, Compensation mechanism, Operational semantics, Axiomatic verification system, Soundness.
Full text:(AM) Accepted Manuscript
Download PDF
Publisher Web site:
Publisher statement:The original publication is available at
Record Created:23 Nov 2009 13:50
Last Modified:02 Dec 2011 16:21

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Look up in GoogleScholar | Find in a UK Library