As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
The refinement of a theoretical model which includes external choice over output and input of a channel transaction into an implementation model is a long-standing 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.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.