Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/85958
Title: | On the monitorability of session types, in theory and practice |
Authors: | Bartolo Burlò, Christian Francalanza, Adrian Scalas, Alceste |
Keywords: | Software engineering Computer communication systems Programming languages (Electronic computers) Computer logic Computer science Scala (Computer program language) |
Issue Date: | 2021 |
Publisher: | Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH |
Citation: | Bartolo Burlò, C., Francalanza, A., & Scalas, A. (2021). On the monitorability of session types, in theory and practice. 35th European Conference on Object-Oriented Programming (ECOOP 2021), Aarhus. 1-30. |
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. |
URI: | https://www.um.edu.mt/library/oar/handle/123456789/85958 |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
On the Monitorability of Session Types.pdf | Primary version of the article | 1.28 MB | Adobe PDF | View/Open |
On the Monitorability of Session Types (extended version).pdf | Extended version of the article. | 1.44 MB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.