Peking Duck Software
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, the authors make one step forward by investigating the verification problem for business processes written in BPEL-like languages. As a result of the exploration, they have proposed a set of Hoare-logic style inference rules which form as an axiomatic verification system for a core BPEL-like language containing key features such as data states, fault and compensation handling.