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.
CITATION STYLE
Schellhorn, G., Bodenmüller, S., Pfähler, J., & Reif, W. (2020). Adding Concurrency to a Sequential Refinement Tower. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12071 LNCS, pp. 6–23). Springer. https://doi.org/10.1007/978-3-030-48077-6_2
Mendeley helps you to discover research relevant for your work.