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.
Gerhard Schellhorn, Stefan Bodenmüller, Jörg Pfähler, Wolfgang Reif. 2020. Adding Concurrency to a Sequential Refinement Tower. Proc. of 7th International Conference ABZ 2020
- Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller, Wolfgang Reif. 2018. Symbolic execution for a clash-free subset of ASMs. Science of Computer Programming
- Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif. 2017. Modular verification of order-preserving write-back caches. Proc. of Integrated Formal Methods 2017
- Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif. 2016. Modular, Crash-Safe Refinement for ASMs with Submachines. Science of Computer Programming
- Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif. 2016. A Relational Encoding for a Clash-Free Subset of ASMs. Proc. of 5th International Conference ABZ 2016
- Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif. 2016. Inside a Verified Flash File System: Transactions & Garbage Collection. Proc. of 7th Working Conference on Verified Software: Theories, Tools and Experiments
Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif. 2014. Development of a Verified Flash File System. Proc. of 4th International Conference ABZ 2014
Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif. 2014. Modular Refinement for Submachines of ASMs. Proc. of 4th International Conference ABZ 2014
Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif. 2014. Crash-Safe Refinement for a Verified Flash File System. Reports / Technische Berichte - Herausgeber: Fakultät für Angewandte Informatik der Universität Augsburg
Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif. 2014. Verification of a Virtual Filesystem Switch.In Proc. of Fifth Working Conference on Verified Software: Theories, Tools and Experiments
Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif. 2013. Formal Specification of an Erase Block Management Layer for Flash Memory. In Proc. of 9th International Haifa Verification Conference
Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif. 2012. A Formal Model of a Virtual Filesystem Switch. In Proc. of Systems Software Verification
Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst. 2011. Simulating a Flash File System with CoreASM and Eclipse. GI Lecture Notes in Informatics 192: Informatik 2011
Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif. 2009. Abstract Specification of the UBIFS File System for Flash Memory. Proceedings of FM 2009: Formal Methods
Institute for Software & Systems Engineering
The Institute for Software & Systems Engineering (ISSE), directed by Prof. Dr. Wolfgang Reif, is a scientific institution within the Faculty of Applied Computer Science of the University of Augsburg. In research, the institute supports both fundamental and application-oriented research in all areas of software and systems engineering. In teaching, the institute facilitates the further development of the faculty's and university's relevant course offerings.