Modelling and analysis of long running transactions

Michael Butler

Business transactions involve hierarchies of activities whose execution needs to be orchestrated. Business transactions typically involve interactions and coordination between multiple partners. The behavior of a transaction can depend on data passed between partners and can involve the manipulation of data. Business transactions also need to deal with faults that arise at any stage of execution. In standard atomic transactions, such as database 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.

Carla Ferreira and I have developed a process language called StAC (Structured Activity Compensation) which models coordination of transactions including exceptions and compensation.A paper on StAC and its operational semantics may be found here:

An Operational Semantics for StAC, a Language for Modelling Long-running Business Transactions.

BPEL4WS (Business Process Execution Language for Web Services) is a web services composition language that is jointly developed by Microsoft, IBM and others. We have done some work on mapping BPEL4WS to StAC (with Karen Ng) which is described here:

Precise Modelling of Compensating Business Transactions and its Application to BPEL.

StAC is used to describe the orchestration of atomic actions and compensations.It is also useful to be able to describe the effect of atomic actions on some abstraction of the data state. The above paper also shows how StAC can be combined with Abrialís B method to achieve this.

Our most recent work is the Compensating CSP language developed together with Tony Hoare.Compensating CSP is simpler but better structured than StAC.This improved structuring has been achieved by working with a denotational semantics which forces us to have operators with compositional definitions.We have developed a correctness criterion for compensating transactions which allows us to combine cancellation assumptions about compensation actions.A recent paper on this can be found here:

A trace semantics for long-running transactions.

Roberto Bruni, Hernan Melgratti and Ugo Montanari are also working on similar ideas and we recently joint forces to write a paper comparing our work:

Comparing two approaches to compensable flow composition

With Shamim Ripon, I have developed an operational semantics for Compensating CSP:

Executable Semantics for Compensating CSP

Carla and I have also investigated the application of refinement to compensating transactions:

Using B Refinement to Analyse Compensating Business Processes.

Our interest in compensating transactions started through collaboration with researchers at IBM Hursley.Some of the results of that collaboration are described here:

Extending the Concept of Transaction Compensation.