Timed runtime monitoring for multiparty conversation
File(s)10.1007%2Fs00165-017-0420-8.pdf (2.12 MB) draft.pdf (1.07 MB)
Published version
Accepted version
Author(s)
Neykova, R
Bocchi, L
Yoshida, N
Type
Journal Article
Abstract
We propose a dynamic verification framework for protocols in real-time distributed systems. The frame-
work is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session
types, which we have developed with our industrial partners. Drawing from recent work on multiparty session types
for real-time interactions, we extend Scribble with clocks, resets, and clock predicates in order to constrain the times
in which interactions occur. We present a timed API for Python to program distributed implementations of Scribble
specifications. A dynamic verification framework ensures the safe execution of applications written with our timed
API: we have implemented dedicated runtime monitors that check that each interaction occurs at a correct timing
with respect to the corresponding Scribble specification. To demonstrate the practicality of the proposed framework,
we express and verify four categories of widely used temporal patterns from use cases in literature. We analyse the
performance of our implementation via benchmarking and show negligible overhead.
work is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session
types, which we have developed with our industrial partners. Drawing from recent work on multiparty session types
for real-time interactions, we extend Scribble with clocks, resets, and clock predicates in order to constrain the times
in which interactions occur. We present a timed API for Python to program distributed implementations of Scribble
specifications. A dynamic verification framework ensures the safe execution of applications written with our timed
API: we have implemented dedicated runtime monitors that check that each interaction occurs at a correct timing
with respect to the corresponding Scribble specification. To demonstrate the practicality of the proposed framework,
we express and verify four categories of widely used temporal patterns from use cases in literature. We analyse the
performance of our implementation via benchmarking and show negligible overhead.
Date Issued
2017-02-22
Date Acceptance
2017-01-16
Citation
Formal Aspects of Computing, 2017, 29 (5), pp.877-910
ISSN
1433-299X
Publisher
Springer Verlag (Germany)
Start Page
877
End Page
910
Journal / Book Title
Formal Aspects of Computing
Volume
29
Issue
5
Copyright Statement
©The Author(s) © 2017. This article is published with open access at Springerlink.com
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
612985
EP/N027833/1
72043/2
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Session types
Protocols
Real time
Runtime monitoring
Verification
Scribble
VERIFICATION
AUTOMATA
0802 Computation Theory And Mathematics
0803 Computer Software
Computation Theory & Mathematics
Publication Status
Published