Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/18462
Title: | Timed runtime monitoring for multiparty conversations |
Authors: | Neykova, R Bocchi, L Yoshida, N |
Keywords: | Session types;Protocols;Real time;Runtime monitoring;Verification;Scribble |
Issue Date: | 2017 |
Publisher: | Springer |
Citation: | Formal Aspects of Computing, 2017, 29 (5), pp. 877 - 910 |
Abstract: | 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, 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 inwhich interactions occur.We present a timedAPI for Python to programdistributed 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. |
URI: | http://bura.brunel.ac.uk/handle/2438/18462 |
DOI: | http://dx.doi.org/10.1007/s00165-017-0420-8 |
ISSN: | http://dx.doi.org/10.1007/s00165-017-0420-8 0934-5043 |
Appears in Collections: | Dept of Computer Science Research Papers |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
FullText.pdf | 2.17 MB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.