Please use this identifier to cite or link to this item:
Title: A Suspension-Trace Semantics for CSP
Authors: Cavalcanti, A
Hierons, RM
Nogueira, S
Sampaio, A
Issue Date: 2016
Publisher: IEEE
Citation: Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 3 - 13, (2016)
Abstract: CSP is well established as a process algebra for refinement. Most refinement relations for CSP do not differentiate between inputs and outputs, and so are unsuitable for testing. This paper provides CSP with a denotational semantics based on suspension traces; it gives the traditional CSP operators a novel view, catering for the differences between inputs and outputs. We identify healthiness conditions for the suspension-Traces model and include a treatment of termination not contemplated in the context of input-output labelled transition systems. Using our suspension-Traces semantics, we provide for CSP a characterisation of the conformance relation ioco, which is widely used in testing. Finally, we propose a strategy to mechanise the verification of conformance according to ioco and suspension-Trace refinement using CSP tools. This work provides the basis for a theory of testing for CSP with inputs and outputs, and opens up the possibility of studying algebraic laws and compositional reasoning techniques based on ioco. Ultimately, it contributes to making CSP models useful for both design and testing of systems.
ISBN: 9781509017638
Appears in Collections:Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
Fulltext.pdf255.76 kBAdobe PDFView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.