2021-08-20
Analysis of specifications of multiparty sessions with dcj-lint
Publication
Publication
Presented at the
29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021 (August 2021), Virtual, Online
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).
| Additional Metadata | |
|---|---|
| , , , | |
| doi.org/10.1145/3468264.3473127 | |
| 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021 | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
Horlings, E., & Jongmans, S. (2021). Analysis of specifications of multiparty sessions with dcj-lint. In Proceedings of the ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering (pp. 1590–1594). doi:10.1145/3468264.3473127 |
|
