A Formal Model of a Virtual Filesystem Switch
Gidon Ernst (University of Augsburg), Gerhard Schellhorn (University, of Augsburg), Dominik Haneberg (University of Augsburg), J\"org Pf\"ahler, (University of Augsburg), Wolfgang Reif (University of Augsburg)
TL;DR
This paper introduces a formal model of a virtual filesystem switch inspired by Linux VFS, enabling verified, POSIX-compatible file system operations for Flash memory with proven correctness and potential for practical implementation.
Contribution
It presents a modular formal model of a virtual filesystem switch that supports verification and can be integrated into Linux, advancing reliable file system design for Flash memory.
Findings
Proved that preconditions of the abstract file system are respected.
Ensured state consistency within the model.
Model can be executed and mounted in Linux using FUSE.
Abstract
This work presents a formal model that is part of our effort to construct a verified file system for Flash memory. To modularize the verification we factor out generic aspects into a common component that is inspired by the Linux Virtual Filesystem Switch (VFS) and provides POSIX compatible operations. It relies on an abstract specification of its internal interface to concrete file system implementations (AFS). We proved that preconditions of AFS are respected and that the state is kept consistent. The model can be made executable and mounted into the Linux directory tree using FUSE.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.