1. On the monitorability of session types, in theory and practice
- Author
-
Bartolo Burlò, Christian, Francalanza, Adrian, Scalas, Alceste, and 35th European Conference on Object-Oriented Programming (ECOOP 2021)
- Subjects
Software engineering ,Scala (Computer program language) ,Session types ,monitorability ,Theory of computation → Concurrency ,Programming languages (Electronic computers) ,Monitor correctness ,Computer science ,Computer logic ,Scala ,Software and its engineering → Software verification and validation ,Software and its engineering → Development frameworks and environments ,monitor correctness ,Computer communication systems ,Monitorability - 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., This work has been partly supported by: the project MoVeMnt (No: 217987-051) under the Icelandic Research Fund; the BehAPI project funded by the EU H2020 RISE under the Marie Skłodowska-Curie action (No: 778233); the EU Horizon 2020 project 830929 CyberSec4Europe; the Danish Industriens Fonds Cyberprogram 2020-0489 Security-by-Design in Digital Denmark., peer-reviewed
- Published
- 2021