×

An extended cCSP with stable failures semantics. (English) Zbl 1286.68312

Cavalcanti, Ana (ed.) et al., Theoretical aspects of computing – ICTAC 2010. 7th international colloquium, Natal, Rio Grande do Norte, Brazil, September 1–3, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14807-1/pbk). Lecture Notes in Computer Science 6255, 121-136 (2010).
Summary: Compensating CSP (cCSP) is an extension to CSP for modeling long-running transactions. It can be used to specify programs of service orchestration written in a programming language like WS-BPEL. So far, only an operational semantics and a trace semantics are given to cCSP. In this paper, we extend cCSP with more operators and define for it a stable failures semantics in order to reason about non-determinism and deadlock. We give some important algebraic laws for the new operators. These laws can be justified and understood from the stable failures semantics. A case study is given to demonstrate the extended cCSP.
For the entire collection see [Zbl 1194.68019].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing

Software:

CCSP
PDFBibTeX XMLCite
Full Text: DOI