Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)

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 mo...

Descripción completa

Detalles Bibliográficos
Autores principales: Bartolo Burlò, Christian, Francalanza, Adrian, Scalas, Alceste
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7281858/
http://dx.doi.org/10.1007/978-3-030-50086-3_13
_version_ 1783544013515653120
author Bartolo Burlò, Christian
Francalanza, Adrian
Scalas, Alceste
author_facet Bartolo Burlò, Christian
Francalanza, Adrian
Scalas, Alceste
author_sort Bartolo Burlò, Christian
collection PubMed
description 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).
format Online
Article
Text
id pubmed-7281858
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-72818582020-06-09 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 Article 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). 2020-05-13 /pmc/articles/PMC7281858/ http://dx.doi.org/10.1007/978-3-030-50086-3_13 Text en © IFIP International Federation for Information Processing 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Bartolo Burlò, Christian
Francalanza, Adrian
Scalas, Alceste
Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)
title Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)
title_full Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)
title_fullStr Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)
title_full_unstemmed Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)
title_short Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)
title_sort towards a hybrid verification methodology for communication protocols (short paper)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7281858/
http://dx.doi.org/10.1007/978-3-030-50086-3_13
work_keys_str_mv AT bartoloburlochristian towardsahybridverificationmethodologyforcommunicationprotocolsshortpaper
AT francalanzaadrian towardsahybridverificationmethodologyforcommunicationprotocolsshortpaper
AT scalasalceste towardsahybridverificationmethodologyforcommunicationprotocolsshortpaper

Ejemplares similares