The development of a fully verified flash file system

Start date: 01.05.2010
Funded by: DFG (Deutsche Forschungsgemeinschaft)
Local head of project: Jörg Pfähler
Local scientists: Stefan Bodenmüller
Gidon Ernst
Dr. Gerhard Schellhorn
Prof. Dr. Wolfgang Reif
Publications: Publication list


The Flashix project aims at the construction and verification of a state-of-the-art file system for flash memory.


The importance of flash memory (solid state disks) compared to traditional hard disks is increasing considerably due to their higher speed and shock resistance. The specific characteristics of flash memory require new file systems. The goal of this projects is a to develop a verified file system for flash memory.

The project has been suggested as pilot for the Verification Grand Challenge, and the results could be practically relevant for NASA. It raises many interesting questions, for which solutions must be developed, e.g. parallel execution of file system operations with caching, interruptibility of all operations (by power failure), ensuring restart to a consistent state, and quantitative assertions about the even usage of all blocks of the file system ("wear leveling").


As a basis for the concepts necessary we will use the flash file system UBIFS, that was integrated into the official Linux kernel in 2008. We will also integrate proposals of other international research groups, that work in parallel on this case study.

We follow a correctness-by-construction approach, namely by incremental refinement from an abstract description of the POSIX file system interface down to executable code. Conceptually, the main refinement steps involve mapping paths as found in the POSIX layer to Inodes (similar to VFS in Linux), introduction of index data structures for persistent/cached file system objects towards the actual erase blocks, using an indirection from logical blocks to support wear-leveling (similar to the UBI layer in UBIFS).

Working with concepts of an open source implementation has the advantage, that our formal development can benefit from realistic requirements like efficiency, solutions and concepts.

The refinement approach has already been applied successfully to the first pilot project of the Grand Challenge (Mondex), and want to enhance and improve the underlying theories for this project. The verification effort will be supported by construction of executable models, to allow early testing and validation of requirements.