Using CSP

This is a tutorial on Communicating Sequential Processes (CSP): a language for modelling patterns of behaviour. It explores the design of the language, and shows how it may be used to construct descriptions of behavioural properties and distributed systems. It explains also how the use of the language may be supported by verification tools. In the next section, we motivate the use of communicating sequential processes to model and reason about complex systems. After that, we present the basic constructs of CSP that can be used to define sequential processes; a number of laws and examples provide the intuition. The semantic models of CSP are the subject of Section 3, where we also introduce the notion of refinement for processes. Sections 4 and 5 present more elaborate CSP constructs to compose processes, including those that model parallel behaviour; again, an extensive number of laws and examples are presented. Data aspects of a system can also be modelled in CSP; this is discussed in Section 6. An important application of CSP is communication protocols; their modelling is discussed in Section 7. Finally, in Section 8, we briefly present the main CSP tools: FDR and Probe. © Springer-Verlag Berlin Heidelberg 2006.