Header menu link for other important links
X
Formal modelling and verification of compensating web transactions
, S. Chakraborty, H.K. Kapoor, K.L. Man
Published in World Scientific Publishing Co.
2012
Pages: 123 - 136
Abstract
Correctness of a system depends on the correct execution of transactions. For large systems, e.g., web-based, these transactions involve more than one component and hence more than one independent entity. Such transactions are called Long Running Transaction(LRT) as they coordinate complex interactions among multiple sub-systems. Well known roll-back mechanism do not suffice to handle faults in LRTs, therefore compensation mechanisms are introduced. However, introduced structures are complex and hard to understand and handle. Formal methods are well known tool for modelling, analysis and synthesis of complex systems. In this chapter we present a technique that allows modelling LRTs using Compensating CSP, then translating them to Promela language and analyzing using SPIN tool. We have modelled and verified the LRTs. We exemplify it using a web service called Air-ticket Reservation System (ATRS). © 2013 by World Scientific Publishing Co. Pte. Ltd. All rights reserved.
About the journal
JournalIAENG Transactions on Electrical Engineering Volume 1: Special Issue of the International Multiconference of Engineers and Computer Scientists 2012
PublisherWorld Scientific Publishing Co.