MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Attribute-Based Transactions in Service Oriented Computing
Laura BOCCHI, Emilio TUOSTO
Mathematical Structures in Computer Science. p. 619 - 665

We present a theory for the design and verifcation of distributed transactions in dynamically reconfgurable systems. Despite several formal approaches have been proposed to study distributed transactional behaviours, the inter-relations between failure propagation and dynamic system reconfguration still need investigation.

We propose a formal model for transactions in Service Oriented Architectures (SOAs) inspired by the attribute mechanisms of the Java Transaction API. Technically, we model services in ATc (after “Attribute-based Transactional calculus”), a CCS-like process calculus where service declarations are decorated with a transactional attribute. Such attribute disciplines, upon service invocation, how the invoked service is executed with respect to the transactional scopes of the invoker. A type system ensures that well-typed ATc systems do not exhibit run-time errors due to misuse of the transactional mechanisms. Finally, we defne a testing framework for distributed transactions in SOAs based on ATc and prove that under reasonable conditions some attributes are observationally indistinguishable.

@article{BT2015,
  author = {Laura Bocchi and Emilio Tuosto},
  title = {{Attribute-Based Transactions in Service Oriented Computing}},
  journal = {MSCS},
  volume = {25},
  issue = {3},
  pages = {619--665},
  publisher = {Cambridge University Press},
  year = 2015
}
@article{BT2015,
  author = {Laura Bocchi and Emilio Tuosto},
  title = {{Attribute-Based Transactions in Service Oriented Computing}},
  journal = {Mathematical Structures in Computer Science},
  volume = {25},
  issue = {3},
  pages = {619--665},
  publisher = {Cambridge University Press},
  doi = "10.1017/S0960129512000904",
  year = 2015
}