Paper Details

Communicating Process Architectures (CPA)
 Title: Transfer Request Broker: Resolving Input-Output Choice
 Conference: Communicating Process Architectures 2008
 Authors: Oliver Faust, Bernhard H. C. Sputh, Alastair Allen
Department of Engineering, University of Aberdeen
 Abstract: 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. 
Files:


BibTeX Entry


Full paper


Presentation