Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/85799
Title: | On the monitorability of session types, in theory and practice (Artifact) |
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: | Leibniz International Proceedings in Informatics |
Citation: | Bartolo Burlò, C., Francalanza, A., & Scalas, A. (2021). On the monitorability of session types, in theory and practice (Artifact). Dagstuhl Artifacts Series, 7(2), 20:2-20: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/85799 |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
DARTS-7-2-2.pdf | 603.55 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.