Analysis of specifications of multiparty sessions with dcj-lint

Erik Horlings; Sung-Shik Jongmans

doi:10.1145/3468264.3473127

Analysis of specifications of multiparty sessions with dcj-lint

Erik Horlings
, Sung-Shik Jongmans

Research Line Resilience (part of LIRS program)

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-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 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	https://doi.org/10.1145/3468264.3473127
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	https://2021.esec-fse.org/ https://dl.acm.org/doi/proceedings/10.1145/3468264

Keywords

Clojure
communication protocols
model checking
specifications

Access to Document

10.1145/3468264.3473127Licence: CC BY

Cite this

Horlings, E., & Jongmans, S.-S. (2021). Analysis of specifications of multiparty sessions with dcj-lint. In D. Spinellis, G. Gousios, M. Chechik, & M. Di Penta (Eds.), ESEC/FSE 2021: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (pp. 1590-1594). ACM Digital Library. https://doi.org/10.1145/3468264.3473127

Horlings, Erik ; Jongmans, Sung-Shik. / Analysis of specifications of multiparty sessions with dcj-lint. ESEC/FSE 2021: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. editor / Diomidis Spinellis ; Georgios Gousios ; Marsha Chechik, ; Massimiliano Di Penta. ACM Digital Library, 2021. pp. 1590-1594

@inproceedings{f701daf6754d45f5ab4a39fba48a2d7b,

title = "Analysis of specifications of multiparty sessions with dcj-lint",

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).",

keywords = "Clojure, communication protocols, model checking, specifications",

author = "Erik Horlings and Sung-Shik Jongmans",

note = "DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.; 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021 ; Conference date: 23-08-2021 Through 28-08-2021",

year = "2021",

month = aug,

doi = "10.1145/3468264.3473127",

language = "English",

isbn = "978-1-4503-8562-6",

pages = "1590--1594",

editor = "Spinellis, \{Diomidis \} and Gousios, \{Georgios \} and \{ Chechik,\}, \{Marsha \} and \{Di Penta\}, \{Massimiliano \}",

booktitle = "ESEC/FSE 2021",

publisher = "ACM Digital Library",

url = "https://2021.esec-fse.org/, https://dl.acm.org/doi/proceedings/10.1145/3468264",

}

Horlings, E & Jongmans, S-S 2021, Analysis of specifications of multiparty sessions with dcj-lint. in D Spinellis, G Gousios, M Chechik, & M Di Penta (eds), ESEC/FSE 2021: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM Digital Library, pp. 1590-1594, 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, 23/08/21. https://doi.org/10.1145/3468264.3473127

Analysis of specifications of multiparty sessions with dcj-lint. / Horlings, Erik; Jongmans, Sung-Shik.
ESEC/FSE 2021: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ed. / Diomidis Spinellis; Georgios Gousios; Marsha Chechik,; Massimiliano Di Penta. ACM Digital Library, 2021. p. 1590-1594.

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Analysis of specifications of multiparty sessions with dcj-lint

AU - Horlings, Erik

AU - Jongmans, Sung-Shik

N1 - Conference code: 29

PY - 2021/8

Y1 - 2021/8

N2 - 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).

AB - 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).

KW - Clojure

KW - communication protocols

KW - model checking

KW - specifications

U2 - 10.1145/3468264.3473127

DO - 10.1145/3468264.3473127

M3 - Conference Article in proceeding

SN - 978-1-4503-8562-6

SP - 1590

EP - 1594

BT - ESEC/FSE 2021

A2 - Spinellis, Diomidis

A2 - Gousios, Georgios

A2 - Chechik,, Marsha

A2 - Di Penta, Massimiliano

PB - ACM Digital Library

T2 - 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Y2 - 23 August 2021 through 28 August 2021

ER -

Horlings E, Jongmans SS. Analysis of specifications of multiparty sessions with dcj-lint. In Spinellis D, Gousios G, Chechik, M, Di Penta M, editors, ESEC/FSE 2021: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM Digital Library. 2021. p. 1590-1594 doi: 10.1145/3468264.3473127

Analysis of specifications of multiparty sessions with dcj-lint

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this