Abstract
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).
Original language | English |
---|---|
Title of host publication | ESEC/FSE 2021 |
Subtitle of host publication | Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering |
Editors | Diomidis Spinellis, Georgios Gousios, Marsha Chechik, Massimiliano Di Penta |
Publisher | ACM Digital Library |
Pages | 1590-1594 |
Number of pages | 5 |
ISBN (Print) | 978-1-4503-8562-6 |
DOIs | |
Publication status | Published - Aug 2021 |
Event | 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering - Athens, Greece Duration: 23 Aug 2021 → 28 Aug 2021 Conference number: 29 https://2021.esec-fse.org/ https://dl.acm.org/doi/proceedings/10.1145/3468264 |
Conference
Conference | 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering |
---|---|
Abbreviated title | ESEC/FSE 2021 |
Country/Territory | Greece |
City | Athens |
Period | 23/08/21 → 28/08/21 |
Internet address |
Keywords
- Clojure
- communication protocols
- model checking
- specifications