A Formal Model of a Virtual Filesystem Switch

Gidon Ernst
(University of Augsburg)
Gerhard Schellhorn
(University of Augsburg)
Dominik Haneberg
(University of Augsburg)
Jörg Pfähler
(University of Augsburg)
Wolfgang Reif
(University of Augsburg)

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.

In Franck Cassez, Ralf Huuck, Gerwin Klein and Bastian Schlich: Proceedings Seventh Conference on Systems Software Verification (SSV 2012), Sydney, Australia, 28-30 November 2012, Electronic Proceedings in Theoretical Computer Science 102, pp. 33–45.
Published: 26th November 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.102.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org