Development of a Verified Flash File System

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

Abstract

This paper gives an overview over the development of a formally verified file system for flash memory. We describe our approach that is based on Abstract State Machines and incremental modular refinement. Some of the important intermediate levels and the features they introduce are given. We report on the verification challenges addressed so far, and point to open problems and future work. We furthermore draw preliminary conclusions on the methodology and the required tool support.

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{SchellhornEPHR14,
  author       = {Gerhard Schellhorn and
                  Gidon Ernst and
                  J{\"{o}}rg Pf{\"{a}}hler and
                  Dominik Haneberg and
                  Wolfgang Reif},
  editor       = {Yamine A{\"{\i}}t Ameur and
                  Klaus{-}Dieter Schewe},
  title        = {Development of a Verified Flash File System},
  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        = {9--24},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-662-43652-3\_2},
  doi          = {10.1007/978-3-662-43652-3\_2},
  timestamp    = {Tue, 07 May 2024 20:13:31 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/SchellhornEPHR14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'14

Related