New evolving internet technologies are extending the role of the World Wide Web from a platform of information exhibition to a new environment for service interactions. While new business opportunities are brought in under this new era of internet, novel challenges are coming out at the same time. Current technologies have been found lacking efficient support for web transactions. Because transactions in the context of web services have distinct features, such as autonomous and interactive, the traditional automatic mechanisms of resource locking and rollback are proved to be inappropriate. For this reason, we suggest that web transactions are constructed through a series of compensable transactions, using the concept of compensation to ensure a relatively relaxed atomicity. This paper formally expresses the composition structures and behavioral dependencies of compensable transactions. Based on the formal description for a transaction model, we are able to further verify its transactional behavior according to the specified requirement of relaxed atomicity and more precise behavioral properties with temporal constraints.


Terminal State State Transition Diagram Partial Compensation Transactional Model Full Compensation 
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.


  1. 1.
    Bocchi, L., Laneve, C., Zavattaro, G.: A calculus for long-running transactions. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 124–138. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Bruni, R., Melgratti, H., Montanari, U.: Theoretical foundations for compensations in flow composition languages. In: POPL 2005, pp. 209–220. ACM Press, New York (2005)Google Scholar
  3. 3.
    Butler, M., Hoare, T., Ferreira, C.: A trace semantics for long-running transaction. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. LNCS, vol. 3525, pp. 133–150. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Butler, M., Ripon, S.: Executable semantics for compensating CSP. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 243–256. Springer, Heidelberg (2005)Google Scholar
  5. 5.
    Elmagarmid, A.K., Leu, Y., Litwin, W., Rusinkiewicz, M.: A multidatabase transaction model for interbase. In: VLDB 1990, pp. 507–518 (1990)Google Scholar
  6. 6.
    Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based verification of Web service compositions. In: ASE 2003, pp. 152–161. IEEE Computer Society, Los Alamitos (2003)Google Scholar
  7. 7.
    Fu, X., Bultan, T., Su, J.: Analysis of interacting BPEL web services. In: Proc. of WWW 2004, pp. 621–630. ACM Press, New York (2004)Google Scholar
  8. 8.
    Garcia-Molina, H., Salem, K.: Sagas. In: Proc. of ACM SIGMOD 1987, pp. 249–259. ACM Press, New York (1987)CrossRefGoogle Scholar
  9. 9.
    Geguang, P., Xiangpeng, Z., Shuling, W., Zongyan, Q.: Towards the Semantics and Verification of BPEL4WS. In: WLFM 2005. ENTCS, vol. 151, pp. 33–52. Elsevier, Amsterdam (2006)Google Scholar
  10. 10.
    Laneve, C., Zavattaro, G.: Foundations of web transactions. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 282–298. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Levy, E., Korth, H.F., Silberschatz, A.: A theory of relaxed atomicity. In: PODC 1991, pp. 95–110. ACM Press, New York (1991)Google Scholar
  12. 12.
    Li, J., Zhu, H., He, J.: Algebraic Semantics for Compensable Transactions. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 306–321. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Li, J., Zhu, H., Pu, G., He, J.: A Formal Model for Compensable Transactions. In: Proc. of ICECCS 2007, pp. 64–73. IEEE Computer Society, Los Alamitos (2007)Google Scholar
  14. 14.
    Li, J., Zhu, H., Pu, G., He, J.: Looking into compensable transactions. In: Proc. of SEW-31, pp. 154–166. IEEE Computer Society, Los Alamitos (2007)Google Scholar
  15. 15.
    Mazzara, M., Lucchi, R.: A framework for generic error handling in business processes. In: WS-FM 2004. ENTCS, vol. 105, pp. 133–145. Elsevier, Amsterdam (2004)Google Scholar
  16. 16.
    Nakajima, S.: Model-checking of safety and security aspects in web service flows. In: Koch, N., Fraternali, P., Wirsing, M. (eds.) ICWE 2004. LNCS, vol. 3140, pp. 488–501. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Ouyang, J., Sahai, A., Machiraju, V.: An approach to optimistic commit and transparent compensation for e-service transactions. HP Laboratories Palo Alto (February 2001)Google Scholar
  18. 18.
    Solanki, M., Cau, A., Zedan, H.: Augmenting semantic web service descriptions with compositional specification. In: WWW 2004, pp. 544–552. ACM Press, New York (2004)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Jing Li
    • 1
  • Huibiao Zhu
    • 1
  • Jifeng He
    • 1
  1. 1.Shanghai Key Laboratory of Trustworthy ComputingEast China Normal UniversityShanghaiChina

Personalised recommendations