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.
Partner
?
F?rderung
?
?
Team
- Telefon: +49 821 598 2124
- Telefon: +49 821 598 2183
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.