Timed Runtime Monitoring for Multiparty Conversations
File(s)1408.5979v1.pdf (584.9 KB)
Published version
Author(s)
Neykova, R
Bocchi, L
Yoshida, N
Type
Journal Article
Abstract
© 2014 Bocchi & N. Yoshida.We propose a dynamic verification framework for protocols in real-time distributed systems. The framework is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session types, 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 constraining the times in which interactions should 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. The performance of our implementation and its practicability are analysed via benchmarking.
Editor(s)
Carbone, M
Date Issued
2014-08-24
Date Acceptance
2014-08-24
Citation
Electronic Proceedings in Theoretical Computer Science, 2014, 162, pp.19-26
ISSN
2075-2180
Publisher
Open Publishing Association
Start Page
19
End Page
26
Journal / Book Title
Electronic Proceedings in Theoretical Computer Science
Volume
162
Copyright Statement
© R. Neykova, L. Bocchi & N. Yoshida
This work is licensed under the
Creative Commons Attribution License.
This work is licensed under the
Creative Commons Attribution License.
License URL
Publication Status
Published