C. Luo
Verifying BPEL-like Programs with Hoare Logic
Luo, C.; Qin, S.; Qiu, Z.
Authors
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. In 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17-19 June 2008, Nanjing, China; proceedings (151-158). https://doi.org/10.1109/tase.2008.41
Conference Name | International Symposium on Theoretical Aspects of Software Engineering |
---|---|
Conference Location | Nanjing, China |
Start Date | Jun 17, 2008 |
End Date | Jun 19, 2008 |
Publication Date | Jun 1, 2008 |
Deposit Date | Nov 23, 2009 |
Publicly Available Date | Nov 8, 2010 |
Publisher | Institute of Electrical and Electronics Engineers |
Pages | 151-158 |
Book Title | 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17-19 June 2008, Nanjing, China; proceedings. |
DOI | https://doi.org/10.1109/tase.2008.41 |
Files
Published Conference Proceeding
(185 Kb)
PDF
Copyright Statement
© 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
You might also like
PTSC: probability, time and shared-variable concurrency
(2009)
Journal Article
Memory Usage Verification Using Hip/Sleek
(2009)
Conference Proceeding
An Interval-based Inference of Variant Parametric Types
(2009)
Conference Proceeding
A Heap Model for Java Bytecode to Support Separation Logic
(2008)
Conference Proceeding
Downloadable Citations
About Durham Research Online (DRO)
Administrator e-mail: dro.admin@durham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search