Synthesis of extended transaction models using ACTA

Abstract

ACTA is a comprehensive transaction framework that facilitates the formal description of properties of extended transaction models. Specifically, using ACTA, one can specify and reason about (1) the effects of transactions on objects and (2) the interactions between transactions. This article presents ACTA as a tool for the synthesis of extended transaction models, one which supports the development and analysis of new extended transaction models in a systematic manner. Here, this is demonstrated by deriving new transaction definitions (1) by modifying the specifications of existing transaction models, (2) by combining the specifications of existing models, and (3) by starting from first principles. To exemplify the first, new models are synthesized from atomic transactions and join transactions. To illustrate the second, we synthesize a model that combines aspect of the nested- and split-transaction models. We demonstrate the latter by deriving the specification of an open-nested-transaction model from high-level requirements.