一句话：提出 dcj-lint，用定制时序逻辑模型检测器检测多参与者会话规约中的缺陷。
多参与者会话类型可用于自动检测协议实现相对规约的违规，但当发现违规时，问题究竟出在实现还是规约并不明确。本文提出 dcj-lint：一个基于多参与者会话类型的规约分析工具，用于发现协议规约本身的缺陷。dcj-lint 借助定制构建的时序逻辑模型检测器，高效执行两类分析：(1) 通用健全性检查；(2) 协议特定性质分析。基准评估显示，dcj-lint 相比现有最先进模型检测器最高快 61 倍，表明其在规约缺陷检测上具有实际效率优势。
Multiparty session types constitute a method to automatically detect violations of protocol implementations relative to specifications. But, when a violation is detected, does it symptomise a bug in the implementation or in the specification? This paper presents dcj-lint: an analysis tool to detect bugs in protocol specifications, based on multiparty session types. By leveraging a custom-built temporal logic model checker, dcj-lint can be used to efficiently perform: (1) generic sanity checks, and (2) protocol-specific property analyses. In our benchmarks, dcj-lint outperforms an existing state-of-the-art model checker (up to 61x faster).