A process algebra in which components communicate through synchronized CSP events. Its operational description uses a labelled transition system; standard observations include CSP traces, CSP stable failures and CSP divergences.[ref]
Rules deriving the labelled transition system of a composite CSP process from transitions of its components.
An algebraic expansion listing the initially possible CSP events and their continuations. It translates operational transition cases into CSP external choice expressions.
For a suitably guarded recursion, two solutions of the same defining equation denote the same CSP process. There is also a mutually recursive version, comparing tuples of solutions.
A representation of a CSP process by specified kinds of observable behaviour. The CSP traces model, CSP stable-failures model and CSP failures-divergences model record progressively more information about refusals and internal activity.
Implementation has only behaviours permitted by specification in CSP semantic model . In particular, CSP traces model refinement means ; the other models additionally constrain CSP stable failures or CSP divergences.
Record CSP stable failures and CSP divergences, treating behaviour after a CSP divergence as unrestricted. This can detect both stable refusal of progress and endless internal activity.
The possibility, after a finite visible CSP trace, of an infinite sequence of consecutive CSP internal actions. The CSP failures-divergences model records this possibility explicitly.[ref]
After CSP trace , the CSP process can reach a CSP stable state offering no event in the refusal set . Refusal is existential over reachable stable alternatives.[ref]
A component specified by possible CSP events and successor behaviours. has no transitions. CSP prefixing, CSP choice and CSP parallel composition construct larger components.
Behave as until it performs a visible CSP event in , then switch to . The triggering event is included in the visible CSP trace.
Allow to proceed while is ready to interrupt. The first visible CSP event of discards and leaves the derivative of . A CSP internal action of alone does not discard .
Relabel visible CSP events according to a function or relation, preserving CSP internal actions. An injective relabelling preserves event identity; a non-injective one can merge distinct actions. In relational renaming, an original event with no image is disabled. Thus partial relational renaming can also restrict an interface.
Events in require both CSP processes; other visible CSP events advance one participant independently. CSP internal actions do not synchronize.
The alphabets assigned to participants determine their shared CSP events. An event in both assigned alphabets requires both participants; one assigned only to a single participant advances that participant. Replicated composition synchronizes all participants whose assigned alphabets contain the event.
The process may internally choose either branch, independently of the environment's offered CSP events. Consequently it can have more CSP stable failures than the corresponding CSP external choice, despite having the same CSP traces.
The first visible CSP event resolves the choice; the environment can select an event offered by only one branch. CSP internal actions can advance a branch without selecting it.
An unobservable transition that the environment cannot block. CSP hiding turns selected visible CSP events into CSP internal actions.
A state with no outgoing CSP internal action. A CSP stable failure records a refusal only after such a state has been reached.
Articles by others on the same topic
Communicating Sequential Processes (CSP) is a formal language used for specifying and reasoning about concurrent systems. It was introduced by British computer scientist Tony Hoare in the late 1970s. CSP provides a framework for designing systems where independent processes can communicate with one another via messages, facilitating coordination and synchronization between the processes. ### Key Concepts of CSP: 1. **Processes**: The basic entities in CSP are processes, which are defined behaviors that can perform actions.