Information Technology Reference
In-Depth Information
local protocol
ResourceAccessControl
class
UserApp(BaseApp):
1
1
at
User
as
U(
role
Controller
as
C,
user, controller, agent =
2
2
role
Agent
as
A) {
[
'User'
,
'Controller'
,
'Agent'
]
3
3
req(duration:
int
)
to
C;
def
start(self):
4
4
interruptible
{
conv = Conversation.create(
5
5
rec
X{
'RACProtocol'
,
'config.yml'
)
6
6
interruptible
{
c = conv.join(user,
'alice'
)
7
7
rec
Y{
# request 1 hour access
8
8
data()
from
A;
c.send(controller,
'req'
, 123)
9
9
continue
Y;
with
c.scope(
'timeout'
,
'stop'
)
10
10
}
as
c1:
11
11
}
with
{
while not
self.limit_reached():
12
12
pause()
by
U;
with
c1.scope(
'pause'
)
as
c2:
13
13
}
while not
buffer.full:
14
14
resume()
to
A;
resource = c2.recv(controller)
15
15
continue
X;
buffer.append(resource)
16
16
}
c2.send_interrupt(
'pause'
)
17
17
}
with
{
# sleep before resume
18
18
stop()
by
U;
c1.send(agent,
'resume'
)
19
19
timeout()
by
C;
if
self.should_stop():
20
20
}
c1.send_interrupt(
'stop'
)
21
21
}
c.close()
22
22
Fig. 5.
Scribble local protocol (left) and Python implementation (right) for the User role
operations at each endpoint is performed by the local conversation library runtime.
The full runtime includes infrastructure for inline monitoring of conversation actions,
while the lightweight version is used with an outline (i.e. externally hosted) monitor. In
both cases, the API enables MPST verification of message exchanges by the monitor by
embedding a small amount of MPST meta data (e.g. conversation identifier, message
kind and operator, source and destination roles), based on the actions and current state
of the endpoint, into the message payload. For each conversation initiated or joined by
an endpoint, the monitor generates an FSM from the local protocol for the role of the
endpoint. The monitor uses the FSM to track the progress of this conversation according
to the protocol, validating each message (via the meta data) as it is sent or received.
3.1
Conversation API
The Python Conversation API offers a high-level interface for safe conversation pro-
gramming, mapping the interaction primitives of session types to lower-level commu-
nication actions on concrete transports. Our current implementation is built over an
AMQP [2] transport. In summary, the API provides the functionality for (1) session
initiation and joining, (2) basic send/receive and (3)
conversation scope
management
for handling interrupt messages. Figure 4 lists the core API operations. The invitation
operations (
create
and
join
) have not been captured in standard MPST systems, but
have formal counterparts in the literature in formalisms such as [11].
We demonstrate the usage of the API in a Python implementation of the local proto-
col projected for the User role. Figure 5 gives the local protocol and its implementation.
Conversation Initiation.
First, the
create
method of the Conversation API (line 5,
right) initiates a new conversation instance of the
ResourceAccessControl
(Figure 2)
protocol, and returns a token that can be used to join the conversation locally. The
