Information Technology Reference
In-Depth Information
U
C
A
req(int)
start
global protocol
ResourceAccessControl(
role
User
as
U,
1
role
Controller
as
C,
role
Agent
as
A) {
2
(1)
req(duration:
int
)
from
U
to
C;
3
// U requests the device for some duration
4
data
start()
from
C
to
A;
5
.
interruptible
{
// U, C and A in scope
6
.
rec
X{
7
(2)
data
interruptible
{
// U and A in scope
8
rec
Y{
9
data()
from
A
to
U;
10
U
C
A
continue
Y;
11
(2)
}
12
}
with
{
// Interrupts A in Y
13
pause
pause()
by
U;
14
}
15
resume()
from
U
to
A;
16
resume
continue
X;
17
(1)
}
18
}
with
{
// Interrupts A and C/U in X
19
stop()
by
U;
// Any time within the duration
20
stop
timeout()
by
C;
// Duration is up
21
}
22
}
23
timeout timeout
Fig. 2.
Sequence diagram (left) and Scribble protocol (right) for the RAC use case
sending a
timeout
message to User and Agent. This is the case where, from Controller's
view, the session has exceeded the requested duration, so Controller interrupts the other
two participants to end the protocol. Note this diagram actually intends that
stop
(and
timeout
) can arise anytime after (1), e.g. between
pause
and
resume
(a notational am-
biguity that is compensated by additional prose comments in the specification).
Interruptible Multiparty Session Types.
Figure 2 (right) shows a Scribble protocol
that formally captures the structure of interaction in the Resource Access Control use
case and demonstrates the uses of our new extension for asynchronous interrupts. Be-
sides the formal foundations, we find the Scribble specification is more explicit and
precise, particularly regarding the combination of compound constructs such as choice
and recursion, than the sequence diagram format, and provides firmer implementation
guidelines for the programmer (demonstrated in
3.1).
A Scribble protocol starts with a header declaring the protocol name (in Figure 2,
ResourceAccessControl
) and role names for the participants (three roles, aliased in the
scope of this protocol definition as
U
,
C
and
A
). Lines 3 and 5 straightforwardly corre-
spond to the first two communications in the sequence diagram. The Scribble syntax
for message signatures, e.g.
req(duration:int)
, means a message with
operator
(i.e.
header, or label)
req
, carrying a
payload
int
annotated as
duration
.The
start()
mes-
sage signature means operator
start
with an empty payload.
We now come to “phase” (1) of the sequence diagram. The new
interruptible
construct captures the informal usage of protocol phases in disciplined manner, making
explicit the interrupt messages and the
scope
in which they apply. Although the syntax
§
