Clojure 中基于运行时验证的通信协议 Discourje -- 终于可以实时了（技术报告）
编程语言
2024-07-02 v1
摘要
多方会话类型（MPST）是一种形式方法，用于简化并发编程。其思想是利用类型检查自动证明实现相对于规范的安全性（协议一致性）和活性（通信死锁自由）。Discourje 是一个基于动态 MPST 的 Clojure 通信协议运行时验证库。原始版本的 Discourje 只能检测安全违规。在本文中，我们 presenting 对 Discourje 的扩展，用于检测也能检测活性违规。
引用
@article{arxiv.2407.00540,
title = {Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last (Technical Report)},
author = {Sung-Shik Jongmans},
journal= {arXiv preprint arXiv:2407.00540},
year = {2024}
}