Abstract
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.
This research was sponsored in part by the grants NSF-CCF-0427202, NSF-CNS-0541606, and NSF-CCF-0546170.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
bpel Specification v 1.1, http://www.ibm.com/developerworks/library/ws-bpel
Business Process Modeling Language bpml, http://www.bpmi.org/
Bruni, R., Butler, M.J., Ferreira, C., Hoare, C.A.R., Melgratti, H.C., Montanari, U.: Comparing two approaches to compensable flow composition. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 383–397. Springer, Heidelberg (2005)
Bruni, R., Melgratti, H., Montanari, U.: Theoretical foundations for compensations in flow composition languages. In: POPL 05, pp. 209–220. ACM Press, New York (2005)
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)
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)
Comon, H., Cortier, V., Mitchell, J.: Tree automata with one memory, set constraints, and ping-pong protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, Springer, Heidelberg (2001)
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
Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web services. In: PODS 04, pp. 71–82. ACM Press, New York (2004)
Fu, X., Bultan, T., Su, J.: Conversation protocols: A formalism for specification and verification of reactive electronic services. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 188–200. Springer, Heidelberg (2003)
Fu, X., Bultan, T., Su, J.: Analysis of interacting bpel web services. In: WWW 04, pp. 621–630. ACM Press, New York (2004)
Garcia-Molina, H., Salem, K.: Sagas. In: SIGMOD 87, pp. 249–259. ACM Press, New York (1987)
Gray, J., Reuter, A.: Transaction processing: Concepts and techniques. Morgan Kaufmann, San Francisco (1993)
Hull, R., Benedikt, M., Christophides, V., Su, J.: E-services: a look behind the curtain. In: PODS 03, pp. 1–14. ACM Press, New York (2003)
Kučera, A., Mayr, R.: Simulation preorder over simple process algebras. Info. and Comp. 173, 184–198 (2002)
Mayr, R.: Decidability of model checking with the temporal logic EF. TCS 256, 31–62 (2001)
Web Services Conversation Language wscl 1.0, http://www.w3.org/TR/wscl10/
wsfl Specification v 1.0, http://www-306.ibm.com/software/solutions/webservices/pdf/WSFL.pdf
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emmi, M., Majumdar, R. (2007). Verifying Compensating Transactions. In: Cook, B., Podelski, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2007. Lecture Notes in Computer Science, vol 4349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69738-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-69738-1_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69735-0
Online ISBN: 978-3-540-69738-1
eBook Packages: Computer ScienceComputer Science (R0)