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"
@InProceedings{Faust08a,
title = "{T}ransfer {R}equest {B}roker: {R}esolving {I}nput-{O}utput {C}hoice",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
author= "Faust, Oliver and Sputh, Bernhard H.C. and Allen, Alastair R.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
editor= "Welch, Peter H. and Stepney, S. and Polack, F.A.C and Barnes, Frederick R. M. and McEwan, Alistair A. and Stiles, G. S. and Broenink, Jan F. and Sampson, Adam T.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
pages = "163--177",
booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2008",
isbn= "978-1-58603-907-3",
year= "2008",
month= "sep",
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."
}