Verifying BPEL-like Programs with Hoare Logic

Luo, C.; Qin, S.; Qiu, Z.

doi:10.1007/s11704-008-0039-2

Verifying BPEL-like Programs with Hoare Logic

Luo, C.; Qin, S.; Qiu, Z.

Authors

C. Luo

S. Qin

Z. Qiu

Abstract

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.

Citation

Luo, C., Qin, S., & Qiu, Z. (2008). Verifying BPEL-like Programs with Hoare Logic. Frontiers of Computer Science in ChinabOnline, 2(4), 344-356. https://doi.org/10.1007/s11704-008-0039-2

Journal Article Type	Article
Publication Date	Dec 1, 2008
Deposit Date	Nov 23, 2009
Publicly Available Date	Dec 11, 2009
Journal	Frontiers of Computer Science in China
Print ISSN	1673-7350
Electronic ISSN	1673-7466
Publisher	Springer
Peer Reviewed	Peer Reviewed
Volume	2
Issue	4
Pages	344-356
DOI	https://doi.org/10.1007/s11704-008-0039-2
Keywords	WS-BPEL, Compensation mechanism, Operational semantics, Axiomatic verification system, Soundness.