We present a tool-based approach for the runtime analysis of communicating processes grounded on probabilistic binary session types. We synthesise a monitor out of a probabilistic session type where each choice point is decorated by a probability distribution. The monitor observes the execution of a process, infers its probabilistic behaviour and issues warnings when the observed behaviour deviates from the one specified by the probabilistic session type.
翻译:我们提出了基于概率二进制会话类型对通信过程进行运行时间分析的基于工具的方法。 我们从概率二进制会话类型中合成一个监测器,其中每个选择点都用概率分布来标注。 监测器观察一个过程的执行情况,推断其概率行为,并在观察到的行为与概率会话类型所指定的行为不同时发出警告。