Transaction Calculus

Abstract

Transaction-based services are increasingly being applied in solving many universal interoperability problems. Exception and failure are the typical phenomena of the execution of long-running transactions. To accommodate these new program features, we extend the Guarded Command Language by addition of compensation and coordination combinators, and enrich the standard design model with new healthiness conditions. The paper proposes a mathematical framework for transactions where a transaction is treated as a mapping from its environment to compensable programs. We provide a transaction refinement calculus, and show that every transaction can be converted to primitive one which simply consists of a forward activity and a compensation module.