On the Monitorability of Session Types, in Theory and Practice (Artifact)

Authors Christian Bartolo Burlò , Adrian Francalanza , Alceste Scalas



PDF
Thumbnail PDF

Artifact Description

DARTS.7.2.2.pdf
  • Filesize: 0.58 MB
  • 3 pages

Document Identifiers

Author Details

Christian Bartolo Burlò
  • Gran Sasso Science Institute, L'Aquila, Italy
Adrian Francalanza
  • Department of Computer Science, University of Malta, Msida, Malta
Alceste Scalas
  • DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark

Acknowledgements

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. The authors would like to thank the anonymous reviewers and Mario Alfonso Prado-Romero for testing the artifact and for providing useful feedback.

Cite As Get BibTex

Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. On the Monitorability of Session Types, in Theory and Practice (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/DARTS.7.2.2

Artifact

  MD5 Sum: d95472f57ddf8852dd7edabf5697e6ae (Get MD5 Sum)

Abstract

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Development frameworks and environments
  • Software and its engineering → Software verification and validation
  • Theory of computation → Concurrency
Keywords
  • Session types
  • monitorability
  • monitor correctness
  • Scala

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Dummy. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail