Modelling and analysis of long running transactions
Business transactions involve hierarchies of activities whose execution needs to be orchestrated. In standard atomic transactions rollback mechanisms are used to protect against faults by providing all or nothing atomicity for transactions. In so-called long running business transactions rollback is not always possible because
parts of a transaction will have been committed or because parts of
a transaction (e.g., communications with external agents)are inherently impossible to undo. In such cases compensation can be used as a way of dealing with faults.
We are developing formal approaches to modelling and analysis of compensating transactions.