π-calculus, Session Types research at Imperial College
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 }