Flashix II: Inkrementelle Verifikation nicht-lokaler Verfeinerungen

• Antragsteller: Professor Dr. Wolfgang Reif
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2010 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 175408244

Im Projekt Flashix geht es um die Verifikation von Flash-Dateisystemen. Flash-Speicher sind bei mobilen und eingebetteten Systemen die mittlerweile dominierende Speichertechnologie, da sie energieeffizienter, schneller sowie stoßsicherer als klassische Speicher sind. Allerdings hängt der Grad der Effizienz und die Lebensdauer sehr von der komplexen Speicherverwaltungsalgorithmik ab, weshalb Flash-Dateisysteme eine große Herausforderung für aktuelle Verifikationssysteme darstellen. In der ersten Phase von Flashix wurde gezeigt, wie man durch bekannte und neue Techniken mit Verfeinerungshierarchien fast alle Verifikationsprobleme in den Griff bekommen kann. Lediglich die Einführung von Nebenläufigkeit, Robustheit gegen Abstürze und nicht-lokalen Effizienzoptimierungen bringen die modulare Verifikation über Verfeinerungshierarchien an ihre praktischen Grenzen. Im Fortsetzungsprojekt wird daher eine Erweiterung zur modularen und inkrementellen Verifikation von nicht-lokalen Verfeinerungen in Refinement-Hierarchien entwickelt, die mit diesen Herausforderungen umgehen kann. Diese Problematik gibt es nicht nur bei Flash-Dateisystemen, sondern in vielen eingebetteten und effizienzkritischen Systemen. Die Verifikationstechnik wird auf das Flashix-Dateisystem angewandt und die Gesamtverifikation abgeschlossen. Ergebnis ist die vollständige Verifikation eines direkt einsetzbaren Flash-Dateisystems, das den POSIX-Standard hoch effizient in C implementiert.

• DFG-Verfahren: Sachbeihilfen