1. On the Monitorability of Session Types, in Theory and Practice (Artifact)
- 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) ,Scalability ,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., peer-reviewed
- Published
- 2021
- Full Text
- View/download PDF