PSTMonitor: Monitor Synthesis from Probabilistic Session Types

TL;DR

PSTMonitor is a tool that verifies message-passing applications at runtime by checking if their probabilistic behaviour aligns with specified session types, analyzing its feasibility and overhead.

Contribution

It introduces PSTMonitor, a novel runtime verification tool for probabilistic session types in message-passing systems, including an analysis of its overhead.

Findings

PSTMonitor effectively detects deviations from expected probabilistic behaviour.

The tool's runtime overhead is manageable for practical applications.

PSTMonitor demonstrates feasibility in real-world scenarios.

Abstract

We present PSTMonitor, a tool for the run-time verification of quantitative specifications of message-passing applications, based on probabilistic session types. The key element of PSTMonitor is the detection of executions that deviate from expected probabilistic behaviour. Besides presenting PSTMonitor and its operation, the paper analyses its feasibility in terms of the runtime overheads it induces.