TY - GEN
T1 - Specifying and verifying Web transactions
AU - Li, Jing
AU - Zhu, Huibiao
AU - He, Jifeng
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/45749085325
U2 - 10.1007/978-3-540-68855-6_10
DO - 10.1007/978-3-540-68855-6_10
M3 - 会议稿件
AN - SCOPUS:45749085325
SN - 3540688544
SN - 9783540688549
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 149
EP - 168
BT - Formal Techniques for Networked and Distributed Systems - FORTE 2008 - 28th IFIP WG 6.1 International Conference, Proceedings
T2 - 28th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2008
Y2 - 10 June 2008 through 13 June 2008
ER -