Monitoring Blackbox Implementations of Multiparty Session Protocols

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).