Liveness of Communicating Transactions (Extended Abstract)
File Type:
PDFItem Type:
Conference PaperDate:
2010Citation:
Edsko de Vries, Vasileios Koutavas and Matthew Hennessy., Liveness of Communicating Transactions (Extended Abstract), 6461, 2010, 392-407Download Item:
Liveness.pdf (Published (author's copy) - Peer Reviewed) 472.4Kb
Abstract:
We study liveness and safety in the context of CCS extended
with communicating transactions, a construct we recently proposed to
model automatic error recovery in distributed systems. We show that
fair-testing and may-testing capture the right notions of liveness and
safety in this setting, and argue that must-testing imposes too strong
a requirement in the presence of transactions. We develop a sound and
complete theory of fair-testing in terms of CCS-like tree failures and show
that, compared to CCS, communicating transactions provide increased
distinguishing power to the observer.We also show that weak bisimilarity
is a sound, though incomplete, proof technique for both may- and fair-
testing. To the best of our knowledge this is the rst semantic treatment
of liveness in the presence of transactions. We exhibit the usefulness of
our theory by proving illuminating liveness laws and simple but non-
trivial examples.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
06 IN.1 189
Author's Homepage:
http://people.tcd.ie/mcbhennehttp://people.tcd.ie/vkoutav
http://people.tcd.ie/devriee
Description:
PUBLISHEDType of material:
Conference PaperSeries/Report no:
6461Availability:
Full text availableDOI:
http://dx.doi.org/10.1007/978-3-642-17164-2_27Licences: