Publications

BibTex format

@article{Neykova:2017:10.1007/s00165-017-0420-8,
author = {Neykova, R and Bocchi, L and Yoshida, N},
doi = {10.1007/s00165-017-0420-8},
journal = {Formal Aspects of Computing},
pages = {877--910},
title = {Timed runtime monitoring for multiparty conversation},
url = {http://dx.doi.org/10.1007/s00165-017-0420-8},
volume = {29},
year = {2017}
}

Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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 sessiontypes, which we have developed with our industrial partners. Drawing from recent work on multiparty session typesfor real-time interactions, we extend Scribble with clocks, resets, and clock predicates in order to constrain the timesin which interactions occur. We present a timed API for Python to program distributed implementations of Scribblespecifications. A dynamic verification framework ensures the safe execution of applications written with our timedAPI: we have implemented dedicated runtime monitors that check that each interaction occurs at a correct timingwith 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 theperformance of our implementation via benchmarking and show negligible overhead.
AU  - Neykova,R
AU  - Bocchi,L
AU  - Yoshida,N
DO  - 10.1007/s00165-017-0420-8
EP  - 910
PY  - 2017///
SN  - 1433-299X
SP  - 877
TI  - Timed runtime monitoring for multiparty conversation
T2  - Formal Aspects of Computing
UR  - http://dx.doi.org/10.1007/s00165-017-0420-8
UR  - http://hdl.handle.net/10044/1/43777
VL  - 29
ER  -

Download

ProfessorNobukoYoshida

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)