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

The process a P offers its environment the opportunity to synchronize on a

in which case it then behaves like P . The process P

→

Q offers its environment
a choice between P and Q based on synchronization with their initial events.
The process P

Q behaves like either P or Q but the choice is made inter-
nally, beyond environmental influence. A third kind of choice, timeout P Q ,
(sometimes called 'sliding choice') combines external and internal influences. It
is represented using internal and external choice by P Q =( P Q .

The process P ; Q behaves like P and, if that terminates, then behaves like Q .
The process P

Q )

A executes the events in the set A internally, without syn-
chronization by its environment; they can be thought of as being replaced by τ
events. The parallel composition P

\

| A | Q requires P and Q to synchronize on

each event a A , but performs other events of P or Q as determined by those

processes. STOP and SKIP are 'atomic' processes; the former models deadlock
by offering no events; the latter models successful termination by offering only

∈

. For example the following process, defined as an abstraction of components
that synchronize on a ,simplyofferstheevent a and then terminates successfully.

( a → SKIP | {a} | ( b → SKIP ; a → SKIP )) \{ b }

CSP has a range of semantic models, the most basic of which are: the traces
model

FD
[9]. In the traces semantics of CSP, a process is represented by the set of all
its possible traces; the result is useful in specifying safety properties. The stable
failures semantics, by recording the refusals of a process, is useful in specifying a
system's safety and liveness properties. In addition to traces and refusals, infinite
sequences of internal transitions ( τ events), called divergences, are required. Di-
vergence can be introduced by hiding, the symbol div and by ill-formed recursion
like P = P . Thus, for example, internal and external choice are indistinguishable
in the traces model but resolved in the stable failures model, whilst divergence
is resolved in the failures-divergences model.
Conformance in CSP is expressed by refinement . Informally, P

T ; the stable failures model F ; and the failures-divergences model

Q means
that Q conforms to P ,orthat Q 's behaviors are contained in those of P .For-
mally, for any of the three semantic models M∈{T , F , FD} ,

P M Q ⇔M ⊆M

[ Q ] [ P ]

where .Theresult

is that CSP provides a refinement calculus supporting process development from
abstract specification to implementation.
Algebraic reasoning is supported by refinement laws that correspond to
containments in the failures-divergences model. Examples are: idempotency of
internal choice, P

M [ P ] denotes the semantics of process P in semantic model M

P = P ; distributivity of internal choice over parallel com-

position, ( P | A | Q ) R =( P R ) | A | ( Q R ); and resolution of nondeter-

minism, P Q P . Using these laws, the timeout operator can also be written

P Q =( P STOP ) Q .