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: