Information Technology Reference
In-Depth Information
Global Protocol
Project
P r o j e c t i o n
Project
Local
Specification
Specification
(Scribble)
Local
Specification
Local
Specification
Source Code
Source Code
Source Code
Conversation
Layer
Implementation
(Python)
Conversation
Layer
Monitor
Conversation
Layer
Verification
(Dynamic)
Monitor
Monitor
Safe Network
Fig. 1.
Scribble methodology from global specification to local runtime verification
In this paper, we present the design and implementation of a framework for dynamic
verification of protocols based on MPST, developed from our collaboration with indus-
try partners [33,28] on the application of MPST theory. In this ongoing work, we are
motivated to adapt MPST to dynamic verification for several reasons. First, session type
checking is typically designed for languages with first-class communication and con-
currency primitives, whereas our collaborations use mainstream engineering languages,
such as Python and Java, that lack the features required to make static session typing
tractable. Distributed systems are also often heterogeneous in nature, meaning that dif-
ferent languages and techniques (e.g. the control flow of an event-driven program is
tricky to verify statically) may be used in the implementation of one system. Dynamic
verification by communication monitoring allows us to verify MPST safety properties
directly for mainstream languages in a more scalable way. Second, a system may use
third-party components or services for which the source code is unavailable for type
checking. Third, certain protocol specification features, such as assertions on specific
message values, can be precisely evaluated at runtime, while static treatments would
usually be more conservative.
Framework Overview.
Figure 1 illustrates the methodology of our framework. The
development of a communication-oriented application starts with the specification of
the intended interactions (the choreography) as a
global
protocol using the Scribble
protocol description language [34], an engineering incarnation of the formal MPST
type language. The core features of Scribble include multicast message passing and
constructs for branching, recursive and parallel conversations. These features support
the specification of a wide range of protocols, from domains such as standard Internet
applications [18], parallel algorithms [27] and Web services [12].
Our toolchain validates that the global protocol satisfies certain well-formedness
properties, such as coherent branches (no ambiguity between participants about which
branch to follow) and deadlock-freedom (between parallel flows). From a well-formed
global protocol, the toolchain mechanically generates (projects) Scribble
local
proto-
cols for each participant (role) defined in the protocol. A local protocol is essentially a
view of the global protocol from the perspective of one role, and provides a more direct
specification for endpoint implementation than the global protocol.
