db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>

%T Specifying and Analysing Networks of Processes in CSPt (or In Search of Associativity)
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
%A  Paul Howells,  Mark d\[rs]Inverno
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
%E Peter H. Welch,  Frederick R. M. Barnes,  Jan F. Broenink,  Kevin Chalmers,  Jan Bækgaard Pedersen,  Adam T. Sampson
%B Communicating Process Architectures 2013
%X In proposing theories of how we should design and specify
   networks of
processes it is necessary to show that the
   semantics of any language
we use to write down the intended
   behaviours of a system has several
qualities.  First in that
   the meaning of what is written on the page
reflects the
   intention of the designer; second that there are
   no
unexpected behaviours that might arise in a specified
   system that are
hidden from the unsuspecting specifier; and
   third that the intention
for the design of the behaviour of
   a network of processes can be
communicated clearly and
   intuitively to others.  In order to achieve
this we have
   developed a variant of CSP, called CSPt, designed to
solve
   the problems of termination of parallel processes present in
   the
original formulation of CSP. In CSPt we introduced three
   parallel
operators, each with a different kind of
   termination semantics, which
we call synchronous,
   asynchronous and race. These operators provide
specifiers
   with an expressive and flexible tool kit to define
   the
intended behaviour of a system in such a way that
   unexpected or
unwanted behaviours are guaranteed not to take
   place.  In this paper
we extend out analysis of CSPt and
   introduce the notion of an alphabet
diagram that illustrates
   the different categories of events that can
arise in the
   parallel composition of processes.  These alphabet
diagrams
   are then used to analyse networks of three processes
   in
parallel with the aim of identifying sufficient
   constraints to ensure
associativity of their parallel
   composition.  Having achieved this we
then proceed to prove
   associativity laws for the three parallel
operators of CSPt.
    Next, we illustrate how to design and construct a
network
   of three processes that satisfy the associativity law,
   using
the associativity theorem and alphabet diagrams. 
   Finally, we outline
how this could be achieved for more
   general networks of processes.