Foundations of Software Systems Group

Liveness and Safety for Communicating Transactions

We propose a novel language construct called communicating transactions, obtained by dropping the isolation requirement from classical transactions, which can be used to model automatic error recovery in distributed systems. We extend CCS with this construct and give a simple semantics for the extended calculus, called TransCCS. We develop a sound and complete theory for both may and fair testing, which we believe are the appropriate notions to capture safety and liveness in TransCCS. We exhibit the usefulness of our theory by proving illuminating laws and simple but non-trivial examples.

Joint work with Edsko de Vries and Vasileios Koutavas

return to the homepage