Monitoring Blackbox Implementations of Multiparty Session Protocols
Bas van den Heuvel, Jorge A. P\'erez, Rares A. Dobre

TL;DR
This paper introduces a framework for distributed monitoring of message-passing networks following multiparty session protocols, supporting blackbox components and complex protocols beyond existing methods.
Contribution
It presents a novel procedure for synthesizing monitors for blackbox components from global types and proves their correctness and transparency.
Findings
Monitors ensure blackboxes correctly follow global session types.
Blackboxes with monitors are behaviorally equivalent to unmonitored ones.
The framework supports protocols previously unmanageable by existing techniques.
Abstract
We present a framework for the distributed monitoring of networks of components that coordinate by message-passing, following multiparty session protocols specified as global types. We improve over prior works by (i) supporting components whose exact specification is unknown ("blackboxes") and (ii) covering protocols that cannot be analyzed by existing techniques. We first give a procedure for synthesizing monitors for blackboxes from global types, and precisely define when a blackbox correctly satisfies its global type. Then, we prove that monitored blackboxes are sound (they correctly follow the protocol) and transparent (blackboxes with and without monitors are behaviorally equivalent).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMobile Agent-Based Network Management · Distributed systems and fault tolerance · Network Traffic and Congestion Control
