Paper Details

%T Transfer Request Broker: Resolving Input\-Output Choice
%A Oliver Faust, Bernhard H.C. Sputh, Alastair R. Allen
%E Peter H. Welch, S. Stepney, F.A.C Polack, Frederick R. M. Barnes, Alistair A. McEwan, G. S. Stiles, Jan F. Broenink, Adam T. Sampson
%B Communicating Process Architectures 2008
%X The refinement of a theoretical model which includes
   external choice over output and input of a channel
   transaction into an implementation model is a longstanding
   problem. In the theory of communicating sequential processes
   this type of external choice translates to resolving input
   and output guards. The problem arises from the fact that
   most implementation models incorporate only input guard
   resolution, known as alternation choice. In this paper we
   present the transaction request broker process which allows
   the designer to achieve external choice over channel ends by
   using only alternation. The resolution of input and output
   guards is refined into the resolution of input guards only.
   To support this statement we created two models. The first
   model requires resolving input and output guards to achieve
   the desired functionality. The second model incorporates the
   transaction request broker to achieve the same functionality
   by resolving only input guards.We use automated model
   checking to prove that both models are trace equivalent.
   The transfer request broker is a single entity which
   resolves the communication between multiple transmitter and
   receiver 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.