@inproceedings{9d3b0479b49c40de9579ceed3397b21b,
title = "Modelling and verification of compensating transactions using the spin tool",
abstract = "Complex transactions are part of the most commonly used systems. Substantial part of such transactions are business transactions. Usually, they coordinate complex interaction among multiple systems, so called Long Running Transactions (LRT). Well known roll-back mechanism does not suffice to handle faults in LRTs, therefore compensation mechanisms are introduced. However, introduced structures are rather complex and hard to be understood and handled. Formal methods are well known tool for modelling, analysis and synthesis of complex systems. In this paper we introduce a work in progress, a technique that allows modelling LRTs using Compensating CSP, then translating them to Promela language and analysing using SPIN tool. We exemplify it using Car Broker Service.",
keywords = "CSP, Compensation Mechanisms, Long Running Transactions, Promela, SPIN",
author = "Kaiyu Wan and Kapoor, {Hemangee K.} and Shirshendu Das and B. Raju and Tomas Krilavicius and Man, {Ka Lok}",
year = "2012",
language = "English",
isbn = "9789881925190",
series = "Lecture Notes in Engineering and Computer Science",
publisher = "Newswood Limited",
pages = "1163--1168",
editor = "Craig Douglas and Jon Burgstone and Ao, {S. I.} and Grundfest, {W. S.}",
booktitle = "International MultiConference of Engineers and Computer Scientists, IMECS 2012",
note = "2012 International MultiConference of Engineers and Computer Scientists, IMECS 2012 ; Conference date: 14-03-2012 Through 16-03-2012",
}