ISSE

Search

Abstract Specification of the UBIFS File System for Flash Memory

Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif

Abstract Specification of the UBIFS File System for Flash Memory

Today we see an increasing demand for flash memory because it has certain advantages like resistance against kinetic shock. However, reliable data storage also requires a specialized file system knowing and handling the limitations of flash memory. This paper develops a formal, abstract model for the UBIFS flash file system, which has recently been included in the Linux kernel. We develop formal specifications for the core components of the file system: the inode-based file store, the flash index, its cached copy in the RAM and the journal to save the differences. Based on these data structures we give an abstract specification of the interface operations of UBIFS and prove some of the most important properties using the interactive verification system KIV.
published 2009 Proceedings of FM 2009: Formal Methods, pages 190-206

Publisher: Springer Berlin / Heidelberg

DOI: http://dx.doi.org/10.1007/978-3-642-05089-3_13


BibTex

For questions regarding the publication, please contact publications@isse.de!


Links: