Multiparty session typing (MPST) is a formal method to make concurrent programming simpler. The idea is to use type checking to automatically prove safety (protocol compliance) and liveness (communication deadlock freedom) of implementations relative to specifications. Discourje is an existing run-time verification library for communication protocols in Clojure, based on dynamic MPST. The original version of Discourje can detect only safety violations. In this paper, we present an extension of Discourje to detect also liveness violations.

翻译：多方会话类型（MPST）是一种简化并发编程的形式化方法，其核心思想是通过类型检查自动证明实现相对于规范的安全性（协议合规性）与活性（通信无死锁）。Discourje是基于动态MPST的现有Clojure通信协议运行时验证库。原始版本的Discourje仅能检测安全性违规。本文提出Discourje的扩展版本，使其能够同时检测活性违规。