Towards a hybrid verification methodology for communication protocols (short paper)

Christian Bartolo Burlò; Adrian Francalanza; Alceste Scalas

doi:10.1007/978-3-030-50086-3_13

Towards a hybrid verification methodology for communication protocols (short paper)

Christian Bartolo Burlò^*, Adrian Francalanza, Alceste Scalas

^*Corresponding author for this work

College of Engineering and Physical Sciences

Research output: Chapter in Book/Published conference output › Conference publication

Abstract

We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels).

Original language	English
Title of host publication	Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings
Editors	Alexey Gotsman, Ana Sokolova
Pages	227-235
Number of pages	9
DOIs	https://doi.org/10.1007/978-3-030-50086-3_13
Publication status	Published - 8 Jun 2020
Event	40th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020 - Valletta, Malta Duration: 15 Jun 2020 → 19 Jun 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12136 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	40th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020
Country/Territory	Malta
City	Valletta
Period	15/06/20 → 19/06/20

Bibliographical note

Keywords

Monitors
Session types
Static and dynamic verification

Access to Document

10.1007/978-3-030-50086-3_13

Cite this

Bartolo Burlò, C., Francalanza, A., & Scalas, A. (2020). Towards a hybrid verification methodology for communication protocols (short paper). In A. Gotsman, & A. Sokolova (Eds.), Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings (pp. 227-235). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12136 LNCS). https://doi.org/10.1007/978-3-030-50086-3_13

Bartolo Burlò, Christian ; Francalanza, Adrian ; Scalas, Alceste. / Towards a hybrid verification methodology for communication protocols (short paper). Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings. editor / Alexey Gotsman ; Ana Sokolova. 2020. pp. 227-235 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{bbb6e47a422546a7addaae5ed09b0671,

title = "Towards a hybrid verification methodology for communication protocols (short paper)",

abstract = "We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels).",

keywords = "Monitors, Session types, Static and dynamic verification",

author = "{Bartolo Burl{\`o}}, Christian and Adrian Francalanza and Alceste Scalas",

note = "{\textcopyright} IFIP International Federation for Information Processing 2020 ; 40th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020 ; Conference date: 15-06-2020 Through 19-06-2020",

year = "2020",

month = jun,

day = "8",

doi = "10.1007/978-3-030-50086-3_13",

language = "English",

isbn = "9783030500856",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "227--235",

editor = "Alexey Gotsman and Ana Sokolova",

booktitle = "Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings",

}

Bartolo Burlò, C, Francalanza, A & Scalas, A 2020, Towards a hybrid verification methodology for communication protocols (short paper). in A Gotsman & A Sokolova (eds), Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12136 LNCS, pp. 227-235, 40th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, 15/06/20. https://doi.org/10.1007/978-3-030-50086-3_13

Towards a hybrid verification methodology for communication protocols (short paper). / Bartolo Burlò, Christian; Francalanza, Adrian; Scalas, Alceste.
Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings. ed. / Alexey Gotsman; Ana Sokolova. 2020. p. 227-235 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12136 LNCS).

Research output: Chapter in Book/Published conference output › Conference publication

TY - GEN

T1 - Towards a hybrid verification methodology for communication protocols (short paper)

AU - Bartolo Burlò, Christian

AU - Francalanza, Adrian

AU - Scalas, Alceste

N1 - © IFIP International Federation for Information Processing 2020

PY - 2020/6/8

Y1 - 2020/6/8

N2 - We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels).

AB - We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels).

KW - Monitors

KW - Session types

KW - Static and dynamic verification

UR - http://www.scopus.com/inward/record.url?scp=85087016888&partnerID=8YFLogxK

UR - https://link.springer.com/chapter/10.1007%2F978-3-030-50086-3_13

U2 - 10.1007/978-3-030-50086-3_13

DO - 10.1007/978-3-030-50086-3_13

M3 - Conference publication

AN - SCOPUS:85087016888

SN - 9783030500856

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 227

EP - 235

BT - Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings

A2 - Gotsman, Alexey

A2 - Sokolova, Ana

T2 - 40th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020

Y2 - 15 June 2020 through 19 June 2020

ER -

Bartolo Burlò C, Francalanza A, Scalas A. Towards a hybrid verification methodology for communication protocols (short paper). In Gotsman A, Sokolova A, editors, Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings. 2020. p. 227-235. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-50086-3_13

Towards a hybrid verification methodology for communication protocols (short paper)

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this