Information Technology Reference
In-Depth Information
projection of Scribble protocols, endpoint implementation, and local FSM genera-
tion.
§
3.1 describes a concise API for conversation programming in Python. The
API decorates conversation messages with the runtime session information required
by the monitors to perform the dynamic verification.
3.2 discusses the monitor im-
plementation, how asynchronous interrupts are handled, and the key architectural
requirements of our framework.
§
§
4 evaluates the performance of our monitor implementation through a collection of
benchmarks. The results show that conversation programming and monitoring can
be realised with low overhead.
The source code of our Scribble toolchain, conversation runtime and monitor, per-
formance benchmarks and further resources are available from the project page [35].
2
Communication Protocols with Asynchronous Interrupts
This section expands on why and how we extend Scribble to support the specification
and verification of asynchronous session interrupts, henceforth referred to as just inter-
rupts. Our running example is based on an OOI project use case, which we have distilled
to focus on session interrupts. Using this example, we outline the technical challenges
of extending Scribble with interrupts.
Resource Access Control (RAC) Use Case.
As is common practice in industry, the cy-
berinfrastructure team of the OOI project [28] manages communication protocol speci-
fications through a combination of informal sequence diagrams and prose descriptions.
Figure 2 (left) gives an abridged version of a sequence diagram given in the OOI doc-
umentation for the Resource Access Control use case [29], regarding access control
of users to sensor devices in the ION Cyberinfrastucture for data acquisition. In the
ION setting, a User interacts with a sensor device via its Agent proxy (which interacts
with the device via a separate protocol outside of this example). ION Controller agents
manage concerns such as authentication of users and metering of service usage.
For brevity, we omit from the diagram some of the data types to be carried in the
messages and focus on the
structure
of the protocol. The depicted interaction can be
summarised as follows. The protocol starts at the top of the left-hand diagram. User
sends Controller a
request
message to use a sensor for a certain amount of time (the
int
in parentheses), and Controller sends a
start
to Agent. The protocol then enters a phase
(denoted by the horizontal line) that we label (1), in which Agent streams
data
messages
(acquired from the sensor) to User. The vertical dots signify that Agent produces the
stream of data freely under its own control, i.e. without application-level control from
User. User and Controller, however, have the option at any point in phase (1) to move
the protocol to the phase labelled (2), below.
Phase (2) comprises three alternatives, separated by dashed lines. In the upper case,
User
interrupts
the stream from Agent by sending Agent a
pause
message. At some
subsequent point, User sends a
resume
and the protocol returns to phase (1). In the mid-
dle case, User interrupts the stream, sending both Agent and Controller a
stop
message.
This is the case where User does not want any more sensor data, and ends the protocol
for all three participants. Finally, in the lower case, Controller interrupts the stream by
