WoTUG - The place for concurrent processes

Paper Details

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

%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"
%A Paul Howells, Mark d'Inverno
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%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.


If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.

Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org

Valid HTML 4.01!