Analysis of specifications of multiparty sessions with dcj-lint
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).
|, , ,|
|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.-S.T.Q. (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