文章基本信息

标题：On the Monitorability of Session Types, in Theory and Practice
本地全文：下载
作者：Bartolo Burlò, Christian ; Francalanza, Adrian ; Scalas, Alceste 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2021
卷号：194
DOI：10.4230/LIPIcs.ECOOP.2021.20
语种：English
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Software components are expected to communicate according to predetermined protocols and APIs. Numerous methods have been proposed to check the correctness of communicating systems against such protocols/APIs. Session types are one such method, used both for static type-checking as well as for run-time monitoring. This work takes a fresh look at the run-time verification of communicating systems using session types, in theory and in practice. On the theoretical side, we develop a formal model of session-monitored processes. We then use this model to formulate and prove new results on the monitorability of session types, defined in terms of soundness (i.e., whether monitors only flag ill-typed processes) and completeness (i.e., whether all ill-typed processes can be flagged by a monitor). On the practical side, we show that our monitoring theory is indeed realisable: we instantiate our formal model as a Scala toolkit (called STMonitor) for the automatic generation of session monitors. These executable monitors can be used as proxies to instrument communication across black-box processes written in any programming language. Finally, we evaluate the viability of our approach through a series of benchmarks.
关键词：Session types;monitorability;monitor correctness;Scala