Abstract
We introduce the syntax that CSP uses to create basic sequential processes: prefixing, recursion and conditional, external and internal choice. The ideas and syntax of events and channels is introduced. We learn the distinction between deterministic and nondeterministic behaviour. Examples include buffer and counter processes, and processes that describe a human’s life in terms of constituent events. We see the ideas of traces and trace refinement. The FDR tool is introduced, as is its input language CSP M .
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This transformation is trivial textually, but less so syntactically since the prefixes move from being part of the operator to become part of the processes being combined, and also we are moving from a single operator of arbitrary ‘arity’ to the repeated use of the binary operator \(\mathrel{\mathord{\Box}}\). The fact that \(\mathrel{\mathord{\Box}}\) is associative (see later) means that the order of this composition is irrelevant.
- 2.
Indeed, in many presentations of CSP they seem to be considered so informal that they are not described as part of the language.
- 3.
RUN could, of course, easily be inserted into the language, but this would create a problem for the many existing scripts that give their own local definitions of it.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer-Verlag London Limited
About this chapter
Cite this chapter
Roscoe, A.W. (2010). Building a Simple Sequential Process. In: Understanding Concurrent Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-1-84882-258-0_1
Download citation
DOI: https://doi.org/10.1007/978-1-84882-258-0_1
Publisher Name: Springer, London
Print ISBN: 978-1-84882-257-3
Online ISBN: 978-1-84882-258-0
eBook Packages: Computer ScienceComputer Science (R0)