Discourje: Runtime Verification of Communication Protocols in Clojure
Ruben Hamers, Sung-Shik Jongmans
Abstract
This paper presents Discourje: a runtime verification framework for communication protocols in Clojure. Discourje guarantees safety of protocol implementations relative to specifications, based on an expressive new version of multiparty session types. The framework has a formal foundation and is itself implemented in Clojure to offer a seamless specification–implementation experience. Benchmarks show Discourje’s overhead can be less than 5% for real/existing concurrent programs.
Topics & Concepts
Computer scienceProgramming languageProtocol (science)Overhead (engineering)ImplementationSession (web analytics)Alternative medicinePathologyMedicineWorld Wide WebLogic, programming, and type systemsFormal Methods in VerificationDistributed systems and fault tolerance