Please use this identifier to cite or link to this item:
Title: How to Verify Your Python Conversations
Authors: Neykova, R
Yoshida, N
Issue Date: Jun-2017
Publisher: River Publishers
Citation: Neykova, R. & Yoshida, N. (2017) 'How to verify your python conversations' in: Gay, S. & Ravara, A. (Eds.). Behavioural Types: from Theory to Tools. Gistrup, Denmark, pp. 77 - 98.
Abstract: In large-scale distributed systems, each application is realised through inter- actions among distributed components. To guarantee safe communication (no deadlocks and communication mismatches) we need programming lan- guages and tools that structure, manage, and policy-check these interactions. Multiparty session types (MSPT), a typing discipline for structured inter- actions between communicating processes, offers a promising approach. To date, however, session types applications have been limited to static verification, which is not always feasible and is often restrictive in terms of programming API and specifying policies. This chapter investigates the design and implementation of a runtime verification framework, ensuring conformance between programs and specifications. Specifications are written in Scribble, a protocol description language formally founded on MPST. The central idea of the approach is a runtime monitor, which takes a form of a communicating finite state machine, automatically generated from Scribble specifications, and a communication runtime stipulating a message format. We demonstrate Scribble-based runtime verification in manifold ways. First, we present a Python library, facilitated with session primi- tives and verification runtime. Second, we show examples from a large cyber-infrastructure project for oceanography, which uses the library as a communication medium. Third, we examine communication patterns, fea- turing advanced Scribble primitives for verification of exception handling behaviours.
ISBN: 8793519826
Other Identifiers: 4
Appears in Collections:Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
FullText.pdf965.56 kBAdobe PDFView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.