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)
NOTE: to access the implementation of the probabilistic monitors switch branch to
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
STMonitoris also published as the companion artifact to the paper.