Failure-divergence semantics and refinement of long running transactions

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

Abstract

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.

Cite

CITATION STYLE

APA

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

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