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).
翻译:我们提出了一种分布式监测框架,用于监控通过消息传递协调的组件网络,这些组件遵循由全局类型指定的多方会话协议。与先前工作相比,我们的改进体现在:(i) 支持具体规格未知的组件(即"黑箱"),(ii) 覆盖现有技术无法分析的协议。我们首先给出了一种从全局类型合成黑箱监测器的方法,并精确定义了黑箱正确满足其全局类型的条件。随后,我们证明被监测的黑箱是可靠的(它们正确遵循协议)且透明的(有无监测器的黑箱行为等价)。