A Suspension-Trace Semantics for CSP

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.