Failure-divergence semantics and refinement of long running transactions

Citations of this article
Mendeley users who have this article in their library.


Compensating CSP (cCSP) models long-running transactions. It can be used to specify service orchestrations written in programming languages like WS-BPEL. However, the original cCSP does not allow to model internal (non-deterministic) choice, synchronized parallel composition, hiding or recursion. In this paper, we introduce these operators and define for the extended language a failure-divergence (FD) semantics to allow reasoning about non-determinism, deadlock and livelock. Furthermore, we develop a refinement calculus that allows us to compare the level of non-determinism between long running transactions, and transform specifications for design and analysis. © 2012 Elsevier B.V. All rights reserved.




Chen, Z., Liu, Z., & Wang, J. (2012). Failure-divergence semantics and refinement of long running transactions. In Theoretical Computer Science (Vol. 455, pp. 31–65).

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free