Modular Refinement for Submachines of ASMs

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
Digital Printed Abstract View Cite
Type
Conference paper
Publication
4th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'14)

Abstract

We describe and formalize a compositional, contract-based submachine refinement for a variant of Abstract State Machines. We motivate the approach by models of the Flash file system case study, where it is infeasible to refine a complete machine as a whole.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{ErnstPSR14,
  author       = {Gidon Ernst and
                  J{\"{o}}rg Pf{\"{a}}hler and
                  Gerhard Schellhorn and
                  Wolfgang Reif},
  editor       = {Yamine A{\"{\i}}t Ameur and
                  Klaus{-}Dieter Schewe},
  title        = {Modular Refinement for Submachines of ASMs},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
                  Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8477},
  pages        = {188--203},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-662-43652-3\_16},
  doi          = {10.1007/978-3-662-43652-3\_16},
  timestamp    = {Tue, 07 May 2024 20:13:31 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/ErnstPSR14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'14

Related