Analysis of specifications of multiparty sessions with dcj-lint

Erik Horlings, Sung-Shik Jongmans

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review

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 languageEnglish
Title of host publicationESEC/FSE 2021
Subtitle of host publicationProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
EditorsDiomidis Spinellis, Georgios Gousios, Marsha Chechik, Massimiliano Di Penta
PublisherACM Digital Library
Pages1590-1594
Number of pages5
ISBN (Print)978-1-4503-8562-6
DOIs
Publication statusPublished - Aug 2021
Event29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering - Athens, Greece
Duration: 23 Aug 202128 Aug 2021
Conference number: 29
https://2021.esec-fse.org/
https://dl.acm.org/doi/proceedings/10.1145/3468264

Conference

Conference29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Abbreviated titleESEC/FSE 2021
Country/TerritoryGreece
CityAthens
Period23/08/2128/08/21
Internet address

Keywords

  • Clojure
  • communication protocols
  • model checking
  • specifications

Fingerprint

Dive into the research topics of 'Analysis of specifications of multiparty sessions with dcj-lint'. Together they form a unique fingerprint.

Cite this