Verifying Compensating Transactions

  • Michael Emmi
  • Rupak Majumdar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)


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.


Business Process Model Check Operational Semantic Regular Language Parallel Composition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
    Business Process Modeling Language bpml,
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 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. 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
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997), Available on
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Fu, X., Bultan, T., Su, J.: Analysis of interacting bpel web services. In: WWW 04, pp. 621–630. ACM Press, New York (2004)CrossRefGoogle Scholar
  12. 12.
    Garcia-Molina, H., Salem, K.: Sagas. In: SIGMOD 87, pp. 249–259. ACM Press, New York (1987)CrossRefGoogle Scholar
  13. 13.
    Gray, J., Reuter, A.: Transaction processing: Concepts and techniques. Morgan Kaufmann, San Francisco (1993)zbMATHGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Kučera, A., Mayr, R.: Simulation preorder over simple process algebras. Info. and Comp. 173, 184–198 (2002)CrossRefGoogle Scholar
  16. 16.
    Mayr, R.: Decidability of model checking with the temporal logic EF. TCS 256, 31–62 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Web Services Conversation Language wscl 1.0,
  18. 18.

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Michael Emmi
    • 1
  • Rupak Majumdar
    • 1
  1. 1.UC Los Angeles 

Personalised recommendations