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). https://doi.org/10.1016/j.tcs.2012.04.040