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

Wissenschaftlicher Mitarbeiter
Institut für Software & Systems Engineering
Wissenschaftlicher Mitarbeiter
Institut für Software & Systems Engineering
Institutsdirektor
Institut für Software & Systems Engineering

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.

Suche