About

STMonitor: Session Types Monitor Synthesiser

Given a session type S, the tool synthesises the Scala code of a type-checked monitor (based on the library lchannels). The monitor verifies at runtime whether the interactions between a client and server follow the protocol S.

The approach and its underlying theory are described in the following papers:

• Christian Bartolo Burlò, Adrian Francalanza and Alceste Scalas. Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper). FORTE 2020. (Pesentation video)

• Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas, Catia Trubiani and Emilio Tuosto. Towards Probabilistic Session-Type Monitoring. COORDINATION 2021. (Pesentation video and Tool demo)

  NOTE: to access the implementation of the probabilistic monitors switch branch to pstmonitor.

• Christian Bartolo Burlò, Adrian Francalanza and Alceste Scalas. On the Monitorability of Session Types, in Theory and Practice. ECOOP 2021. (Pesentation video). This version of STMonitor is also published as the companion artifact to the paper.