Information Technology Reference
In-Depth Information
mainstream languages, however, requires support in the form of the language
extensions and pre-compiler processing to be tractable.
In this paper, we demonstrate a toolchain (SPY: Session Python) for runtime
verification of distributed Python programs against Scribble protocol specifica-
tions. Our aim is to adapt the MPST protocol verification techniques to runtime
verification in order to be directly applicable to standard mainstream languages.
Due to the distributed setting, our toolchain works to enforce a
global
proto-
col by decomposing it into
local
specifications to be independently monitored
at each endpoint. Runtime verification can also be more practical for enforc-
ing advanced protocol features, e.g. we have extended our version of Scribble to
support annotations for logical assertions, which would be more complicated to
verify statically, even conservatively and with language extensions.
Given a Scribble specification of a global protocol, our toolchain validates
consistency properties, such as race-free branch paths, and generates Scribble
(i.e. syntactic) local protocol specifications for each participant (role) defined
in the protocol. At runtime, an independent monitor (internal or external) is
assigned to each Python endpoint. When a session between the endpoints is
initiated, each monitor retrieves the local protocol for its endpoint, and generates
the corresponding finite state machine (by an extension of the algorithm in [4])
to verify the local trace of communication actions executed during the session.
The evaluation of assertions is handled through a third-party engine.
To summarise the main features and characteristics of our toolchain: (1) it
is based on a specification language [6,12] with a formal semantics [3,2] (with
proof of the soundness of local monitoring of global protocols), and is the first
implementation of runtime verification for this theory; (2) protocol specifications
can be decorated to perform third-party validation of constraints beyond the core
message passing protocol; (3) monitoring is decentralised with each participant
verified locally and therefore no synchronisation between monitors is needed;
(4) two kinds of monitor, internal (synchronous) and external (asynchronous),
are implemented; and (5) the toolchain has been integrated into an industry
project [10] for the verification of RPC services and multiagent protocols [11].
The rest of the paper illustrates the key steps of the toolchain, outline its
usage requirements and discusses current applications. A discussion of related
work and additional examples can be found within the same volume [8]. The
source code of the tools and performance benchmarks are available from the
project website [9].
2 Multiparty Session Types and Runtime Verification
We illustrate our toolchain through an introductory example, an online pay-
ment application, which we call OnlineWallet (Fig. 1). The scenario involves
three parties: a Client (C), a Payment Server (S) and a separate Authentica-
tor (A). At the start of a session, C sends its login details to A, and A replies
to inform C and S whether the authentication is successful or not. If so, C and
