Flashix
Projekt Überblick
Die Bedeutung von Flash-Speicher (Solid State Disks) verglichen zu herkömmlichem Magnet-Speicher steigt stetig an, bedingt durch dessen höhere Geschwindigkeit und Stoßfestigkeit. Die besonderen Charakteristika von Flash-Speicher erfordern neue Dateisysteme. Ziel des Flashix Projektes ist die Entwicklung eines verifizierten Dateisystems für Flash-Speicher.
Das Projekt wurde als Pilot-Projekt der Verification Grand Challenge vorgeschlagen und die Ergebnisse könnten praktisch relevant für die NASA sein. Im Rahmen des Projekts werden viele interessante Forschungsfragen angegangen, wie z.B. die parallele Ausführung von Dateisystemoperationen im Zusammenspiel mit Caching-Mechanismen, die Unterbrechbarkeit von allen Operationen (durch Stromausfälle), die Garantie eines Neustarts in einen konsistenten Zustand und quantitative Zusicherungen über die gleichmäßige Nutzung aller Blöcke des Dateisystems (sog. „Wear Leveling“).
Als Grundlage für die notwendigen Konzepte dient das Flash-Dateisystem UBIFS, das 2008 in den offiziellen Linux Kernel integriert wurde. Es werden außerdem Vorschläge von anderen internationalen Forschungsgruppen, die parallel an dieser Fallstudie arbeiten, mit einbezogen.
Wir verfolgen einen Correctness-by-Construction Ansatz, indem inkrementell eine abstrakte Spezifikation der POSIX Dateisystem Schnittstelle hin zu ausführbarem Code verfeinert wird. Konzeptionell bestehen die wichtigsten Verfeinerungsschritte darin, Pfade, wie sie in der POSIX-Schicht zu finden sind, auf Inodes abzubilden (ähnlich wie VFS in Linux), Indexdatenstrukturen für persistente/gecachte Dateisystemobjekte in Richtung der eigentlichen Erase Blocks einzuführen, wobei eine Indirektion von logischen Blöcken zur Unterstützung des Wear-Levelings verwendet wird (ähnlich der UBI-Schicht in UBIFS).
Die Arbeit mit Konzepten einer Open Source Implementierung hat den Vorteil, dass unsere formale Entwicklung von realistischen Anforderungen (wie Effizienz), Lösungen und Konzepten profitieren kann.
Der Verfeinerungsansatz wurde bereits erfolgreich auf das erste Pilotprojekt der Grand Challenge (Mondex) angewendet und soll die diesem Projekt zugrunde liegenden Theorien erweitern und verbessern. Der Verifikationsaufwand wird durch den Aufbau von ausführbaren Modellen unterstützt, um ein frühzeitiges Testen und Validieren der Anforderungen zu ermöglichen.
Team
- Telefon: +49 821 598 2124
Veröffentlichungen
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
Institut für Software & Systems Engineering
Das Institut für Software & Systems Engineering, geleitet von Prof. Dr. Wolfgang Reif, ist eine wissenschaftliche Einrichtung in der Fakultät für Angewandte Informatik an der Universität Augsburg. Das Institut unterstützt sowohl Grundlagen- als auch angewandte Forschung in allen Bereichen der Software & Systems Engineering. In der Lehre ermöglicht es die weitere Entwicklung des relevanten Kursangebots von Fakultät und Universität.