More Web Proxy on the site http://driver.im/

Article

Specifying and Verifying Web Transactions

Authors:

Jifeng HeAuthors Info & Claims

FORTE '08: Proceedings of the 28th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems

Pages 149 - 168

https://doi.org/10.1007/978-3-540-68855-6_10

Published: 10 June 2008 Publication History

Abstract

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.

References

[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).

[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).

[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).

[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).

[5]

Elmagarmid, A.K., Leu, Y., Litwin, W., Rusinkiewicz, M.: A multidatabase transaction model for interbase. In: VLDB 1990, pp. 507-518 (1990).

[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).

[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).

[8]

Garcia-Molina, H., Salem, K.: Sagas. In: Proc. of ACM SIGMOD 1987, pp. 249- 259. ACM Press, New York (1987).

[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).

[10]

Laneve, C., Zavattaro, G.: Foundations of web transactions. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 282-298. Springer, Heidelberg (2005).

[11]

Levy, E., Korth, H.F., Silberschatz, A.: A theory of relaxed atomicity. In: PODC 1991, pp. 95-110. ACM Press, New York (1991).

[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).

[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).

[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).

[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).

[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).

[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).

[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).

Cited By

Casado RTuya JYounas M(2015)Evaluating the effectiveness of the abstract transaction model in testing Web services transactionsConcurrency and Computation: Practice & Experience10.1002/cpe.285127:4(765-781)Online publication date: 25-Mar-2015
https://dl.acm.org/doi/10.1002/cpe.2851
Colombo CPace G(2013)Recovery within long-running transactionsACM Computing Surveys10.1145/2480741.248074545:3(1-35)Online publication date: 3-Jul-2013
https://dl.acm.org/doi/10.1145/2480741.2480745
Casado RTuya JYounas MOssowski SLecca P(2012)Testing the reliability of web services transactions in cooperative applicationsProceedings of the 27th Annual ACM Symposium on Applied Computing10.1145/2245276.2245418(743-748)Online publication date: 26-Mar-2012
https://dl.acm.org/doi/10.1145/2245276.2245418
Show More Cited By

Specifying and Verifying Web Transactions
1. Information systems
  1. World Wide Web

Recommendations

Invalidating transactions: optimizations, theory, guarantees, and unification
Fast software transactions
Towards formally specifying and verifying transactional memory
Abstract
Over the last decade, great progress has been made in developing practical transactional memory (TM) implementations, but relatively little attention has been paid to precisely specifying what it means for them to be correct, or formally proving ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FORTE '08: Proceedings of the 28th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems

June 2008

339 pages

ISBN:9783540688549

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 10 June 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Casado RTuya JYounas M(2015)Evaluating the effectiveness of the abstract transaction model in testing Web services transactionsConcurrency and Computation: Practice & Experience10.1002/cpe.285127:4(765-781)Online publication date: 25-Mar-2015
https://dl.acm.org/doi/10.1002/cpe.2851
Colombo CPace G(2013)Recovery within long-running transactionsACM Computing Surveys10.1145/2480741.248074545:3(1-35)Online publication date: 3-Jul-2013
https://dl.acm.org/doi/10.1145/2480741.2480745
Casado RTuya JYounas MOssowski SLecca P(2012)Testing the reliability of web services transactions in cooperative applicationsProceedings of the 27th Annual ACM Symposium on Applied Computing10.1145/2245276.2245418(743-748)Online publication date: 26-Mar-2012
https://dl.acm.org/doi/10.1145/2245276.2245418
Mashiyat ARabbi FMacCaull W(2011)Modeling and verifying timed compensable workflows and an application to health careProceedings of the 16th international conference on Formal methods for industrial critical systems10.5555/2037070.2037088(244-259)Online publication date: 29-Aug-2011
https://dl.acm.org/doi/10.5555/2037070.2037088
MacCaull WRabbi F(2011)NOVA workflowProceedings of the First international conference on Foundations of Health Informatics Engineering and Systems10.1007/978-3-642-32355-3_5(75-92)Online publication date: 29-Aug-2011
https://dl.acm.org/doi/10.1007/978-3-642-32355-3_5
Rabbi FWang HMacCaull W(2010)Compensable workflow netsProceedings of the 12th international conference on Formal engineering methods and software engineering10.5555/1939864.1939877(122-137)Online publication date: 17-Nov-2010
https://dl.acm.org/doi/10.5555/1939864.1939877

View Options

View options

Figures

Tables

Media

View Table of Conten