License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2021.20
URN: urn:nbn:de:0030-drops-140630
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14063/
Go to the corresponding LIPIcs Volume Portal

Bartolo Burlò, Christian ; Francalanza, Adrian ; Scalas, Alceste

On the Monitorability of Session Types, in Theory and Practice

pdf-format:
LIPIcs-ECOOP-2021-20.pdf (1 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{bartoloburlo_et_al:LIPIcs.ECOOP.2021.20,
  author =	{Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
  title =	{{On the Monitorability of Session Types, in Theory and Practice}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{20:1--20:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14063},
  URN =		{urn:nbn:de:0030-drops-140630},
  doi =		{10.4230/LIPIcs.ECOOP.2021.20},
  annote =	{Keywords: Session types, monitorability, monitor correctness, Scala}
}

Keywords: Session types, monitorability, monitor correctness, Scala
Collection: 35th European Conference on Object-Oriented Programming (ECOOP 2021)
Issue Date: 2021
Date of publication: 06.07.2021
Supplementary Material: Software (ECOOP 2021 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.7.2.2

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI