Flashix
Project Overview
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.
Team
Publications
2023
- Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif. 2023. Refinement and Separation – Modular Verification of Wandering Trees. Proc. of 18th International Conference on Integrated Formal Methods 2023
- Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif. 2023. Separating Separation Logic – Modular Verification of Red-Black Trees. Proc. of 14th International Conference on Verified Software: Theories, Tools and Experiments 2022
2022
- Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif. 2022. Verification of Crashsafe Caching in a Virtual File System Switch. Formal Aspects of Computing
2021
- Stefan Bodenmüller, Gerhard Schellhorn, Martin Bitterlich, Wolfgang Reif. 2021. Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System. Logic, Computation and Rigorous Methods - Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday
2020
-
Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif. 2020. Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch. Proc. of 16th International Conference on Integrated Formal Methods 2020
-
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
2018
- 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
2017
- Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif. 2017. Modular Verification of Order-Preserving Write-Back Caches. Proc. of 13th International Conference on Integrated Formal Methods 2017
2016
- 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
2014
-
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. Proc. of 5th Working Conference on Verified Software: Theories, Tools and Experiments
2013
-
Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif. 2013. Formal Specification of an Erase Block Management Layer for Flash Memory. Proc. of 9th International Haifa Verification Conference
2012
-
Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif. 2012. A Formal Model of a Virtual Filesystem Switch. Proc. of Systems Software Verification
2011
-
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
2009
-
Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif. 2009. Abstract Specification of the UBIFS File System for Flash Memory. Proc. of FM 2009: Formal Methods
Links
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.