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. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Schellhorn, G., Ernst, G., Pfähler, J., Haneberg, D., & Reif, W. (2014). Development of a verified flash file system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8477 LNCS, pp. 9–24). Springer Verlag. https://doi.org/10.1007/978-3-662-43652-3_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
