Adding Concurrency to a Sequential Refinement Tower

This paper defines a concept and a verification methodology for adding concurrency to a sequential refinement tower of abstract state machines, that is based on data refinement and a component structure. We have developed such a refinement tower for the Flashix file system earlier, from which we gen...

Descripción completa

Detalles Bibliográficos
Autores principales: Schellhorn, Gerhard, Bodenmüller, Stefan, Pfähler, Jörg, Reif, Wolfgang
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7242096/
http://dx.doi.org/10.1007/978-3-030-48077-6_2
_version_ 1783537180362145792
author Schellhorn, Gerhard
Bodenmüller, Stefan
Pfähler, Jörg
Reif, Wolfgang
author_facet Schellhorn, Gerhard
Bodenmüller, Stefan
Pfähler, Jörg
Reif, Wolfgang
author_sort Schellhorn, Gerhard
collection PubMed
description This paper defines a concept and a verification methodology for adding concurrency to a sequential refinement tower of abstract state machines, that is based on data refinement and a component structure. We have developed such a refinement tower for the Flashix file system earlier, from which we generate executable (C and Scala) Code. The question we answer in this paper, is how to add concurrency based on locks to such a refinement tower, without breaking the initial modular structure. We achieve this by just enhancing the relevant components, and adding intermediate atomicity refinements that complement the data refinements that are already there. We also give a verification methodology for such atomicity refinements.
format Online
Article
Text
id pubmed-7242096
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-72420962020-05-22 Adding Concurrency to a Sequential Refinement Tower Schellhorn, Gerhard Bodenmüller, Stefan Pfähler, Jörg Reif, Wolfgang Rigorous State-Based Methods Article This paper defines a concept and a verification methodology for adding concurrency to a sequential refinement tower of abstract state machines, that is based on data refinement and a component structure. We have developed such a refinement tower for the Flashix file system earlier, from which we generate executable (C and Scala) Code. The question we answer in this paper, is how to add concurrency based on locks to such a refinement tower, without breaking the initial modular structure. We achieve this by just enhancing the relevant components, and adding intermediate atomicity refinements that complement the data refinements that are already there. We also give a verification methodology for such atomicity refinements. 2020-04-22 /pmc/articles/PMC7242096/ http://dx.doi.org/10.1007/978-3-030-48077-6_2 Text en © Springer Nature Switzerland AG 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
Schellhorn, Gerhard
Bodenmüller, Stefan
Pfähler, Jörg
Reif, Wolfgang
Adding Concurrency to a Sequential Refinement Tower
title Adding Concurrency to a Sequential Refinement Tower
title_full Adding Concurrency to a Sequential Refinement Tower
title_fullStr Adding Concurrency to a Sequential Refinement Tower
title_full_unstemmed Adding Concurrency to a Sequential Refinement Tower
title_short Adding Concurrency to a Sequential Refinement Tower
title_sort adding concurrency to a sequential refinement tower
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7242096/
http://dx.doi.org/10.1007/978-3-030-48077-6_2
work_keys_str_mv AT schellhorngerhard addingconcurrencytoasequentialrefinementtower
AT bodenmullerstefan addingconcurrencytoasequentialrefinementtower
AT pfahlerjorg addingconcurrencytoasequentialrefinementtower
AT reifwolfgang addingconcurrencytoasequentialrefinementtower

Ejemplares similares