Simulating Truly Concurrent CSP - Formal Methods: Foundations and Applications - page 129

of reasoning about things like data values and execution of procedures. Examples
of systems that allow execution of user-defined functions when an event occurs
are CSP-OZ [1], CSP++ [2] and the Process Analysis Toolkit PAT [11]. Such sys-
tems separate execution of user-defined functions from one another (they are not
executed in parallel) or disallow user-defined functions on synchronization events.
Those assumptions limit the gains promised by concurrency.
An important consequence of the approach taken here is that sets of events
that may occur concurrently are computed statically. As a result, the approach
appears suitable for realistic simulation (in the sense that functions attached
to events may be executed concurrently but may require positive duration),
overcoming the limitations mentioned in the previous paragraph. Indeed any
event (even synchronization events) can be linked to a terminating user-defined
function, and the functions executed concurrently. A user-defined function is
started immediately after its corresponding start (non-tick) event and after its
termination the corresponding end event becomes available.
Sect. 2 provides an overview of CSP and introduces its tools required in this
paper. Sect. 3 introduces the transformation T that performs splitting of events,
then Sect. 4 shows how the transformed process can be used to compose a sys-
tem that simulates the original process while collecting concurrency information.
Sect. 5 presents properties used to prove that the construction preserves the se-
mantics of the original process. Three examples are presented in Sect. 6, though
they may be browsed earlier. Limitations, related and further work are discussed
in Sect. 7. The conclusion is presented in Sect. 8.

2CSP

The process calculus Communicating Sequential Processes (CSP), introduced
by Hoare in the late 1970s, was largely stable by the mid 1980s [4] since when
it has been widely applied and developed. Its strength is the specification and
verification of reactive and concurrent systems in which synchronization and
communication play a key role. Its processes perform events that are both atomic
and instantaneous. The set of events that may be communicated by a process
is said to comprise its alphabet Σ . If a process offers an event with which its
environment agrees to synchronize, the event is performed. A sequence of events
that a process may perform is called a trace of the process. For (semantic)
convenience the alphabet of each process is extended to contain two further
events: τ/

Σ represents termination.
Processes are patterns of computation observable, in the standard model, by
the sets (because of nondeterminism) of events on which they may refuse to
synchronize at any point in their evolution, as determined by the trace that has
been performed; the trace/set pair is called a failure . A process can be thought
of as a (possibly infinite) transition system.
CSP is equipped with a rich set of process operators including prefixing

∈ Σ represents an internal event and ∈ /

( a → P ), external choice ( P Q ), internal choice ( P Q ), sequential composi-

tion ( P ; Q ), abstraction or hiding ( P \ A ) and parallel composition ( P | A | Q ).