Verifying Compensating Transactions
We study the safety verification problem for business-process orchestration languages with respect to regular properties. Business transactions involve long-running distributed interactions between multiple partners which must appear as a single atomic action. This illusion of atomicity is maintained through programmer-specified compensation actions that get run to undo previous actions when certain parts of the transaction fail to finish. Programming languages for business process orchestration provide constructs for declaring compensation actions, which are co-ordinated by the run time system to provide the desired transactional semantics. The safety verification problem for business processes asks, given a program with programmer specified compensation actions and a regular language specifying “good” behaviors of the system, whether all observable action sequences produced by the program are contained in the set of good behaviors.
We show that the usual trace-based semantics for business process languages leads to an undecidable verification problem, but a tree-based semantics gives an algorithm that runs in time exponential in the size of the business process. Our constructions translate programs with compensations to tree automata with one memory.
KeywordsBusiness Process Model Check Operational Semantic Regular Language Parallel Composition
Unable to display preview. Download preview PDF.
- 1.bpel Specification v 1.1, http://www.ibm.com/developerworks/library/ws-bpel
- 2.Business Process Modeling Language bpml, http://www.bpmi.org/
- 5.Butler, M., Ferreira, C.: An operational semantics for StAC, a language for modeling business transactions. In: Druschel, P., Kaashoek, M.F., Rowstron, A. (eds.) IPTPS 2002. LNCS, vol. 2429, pp. 87–104. Springer, Heidelberg (2002)Google Scholar
- 6.Butler, M., Hoare, C.A.R., Ferreira, C.: A trace semantics for long-running transactions. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. LNCS, vol. 3525, pp. 133–150. Springer, Heidelberg (2005)Google Scholar
- 8.Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997), Available on http://www.grappa.univ-lille3.fr/tata
- 17.Web Services Conversation Language wscl 1.0, http://www.w3.org/TR/wscl10/
- 18.wsfl Specification v 1.0, http://www-306.ibm.com/software/solutions/webservices/pdf/WSFL.pdf