Timed Runtime Monitoring for Multiparty Conversations
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 multipa...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1408.5979v1 |
| _version_ | 1817980742642171904 |
|---|---|
| author | Rumyana Neykova Laura Bocchi Nobuko Yoshida |
| author_facet | Rumyana Neykova Laura Bocchi Nobuko Yoshida |
| author_sort | Rumyana Neykova |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T22:57:09Z |
| format | Article |
| id | doaj.art-e220bd2c994b4e5aa18fc299d2989842 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T22:57:09Z |
| publishDate | 2014-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-e220bd2c994b4e5aa18fc299d29898422022-12-22T02:25:58ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-08-01162Proc. BEAT 2014192610.4204/EPTCS.162.3:1Timed Runtime Monitoring for Multiparty ConversationsRumyana Neykova0Laura Bocchi1Nobuko Yoshida2 Imperial College London Imperial College London Imperial College London 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.http://arxiv.org/pdf/1408.5979v1 |
| spellingShingle | Rumyana Neykova Laura Bocchi Nobuko Yoshida Timed Runtime Monitoring for Multiparty Conversations Electronic Proceedings in Theoretical Computer Science |
| title | Timed Runtime Monitoring for Multiparty Conversations |
| title_full | Timed Runtime Monitoring for Multiparty Conversations |
| title_fullStr | Timed Runtime Monitoring for Multiparty Conversations |
| title_full_unstemmed | Timed Runtime Monitoring for Multiparty Conversations |
| title_short | Timed Runtime Monitoring for Multiparty Conversations |
| title_sort | timed runtime monitoring for multiparty conversations |
| url | http://arxiv.org/pdf/1408.5979v1 |
| work_keys_str_mv | AT rumyananeykova timedruntimemonitoringformultipartyconversations AT laurabocchi timedruntimemonitoringformultipartyconversations AT nobukoyoshida timedruntimemonitoringformultipartyconversations |