,
Adrian Francalanza
,
Alceste Scalas
Creative Commons Attribution 4.0 International license
d95472f57ddf8852dd7edabf5697e6ae
(Get MD5 Sum)
In the paper "On the Monitorability of Session Types, in Theory and Practice" we study the monitorability of message-passing black-box processes against protocol specifications expressed as session types; we formalise a monitor synthesis procedure, prove its correctness, and discuss its implementation - as a tool that synthesises an executable monitor (in the Scala programming language) from a given session type. This artifact contains the aforementioned monitor synthesis tool, called STMonitor; it includes the tool source code, and documentation to reproduce the examples and benchmarks described in the paper.
@Article{bartoloburlo_et_al:DARTS.7.2.2,
author = {Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
title = {{On the Monitorability of Session Types, in Theory and Practice (Artifact)}},
pages = {2:1--2:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2021},
volume = {7},
number = {2},
editor = {Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.7.2.2},
URN = {urn:nbn:de:0030-drops-140267},
doi = {10.4230/DARTS.7.2.2},
annote = {Keywords: Session types, monitorability, monitor correctness, Scala}
}