Crash-Safe Refinement for a Verified Flash File System

Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg and Wolfgang Reif

Crash-Safe Refinement for a Verified Flash File System

This technical report presents formal proof obligations for data refinement in the presence of unexpected crashes, notably due to a power failure. The work is part of our effort to construct a verified file system for flash memory. We apply the theory to one of the components in the flash file system, namely the erase block management layer. We show its functional correctness with respect to a high-level specification. We prove that the system can always recover from power loss to a desired state. We observe two simplifications that greatly reduce the proof effort for crashes in practice. Proofs are mechanized in the theorem prover KIV.

Download PDF
published 2014 in: Augsburg Reports / Technische Berichte - Herausgeber: Fakultät für Angewandte Informatik der Universität Augsburg

Publisher: OPUS, Report 2014-02


For questions regarding the publication, please contact!