IKCEST

Electronic Proceedings in Theoretical Computer Science | Vol.102, Issue.Proc. SSV 2012 | | Pages

A Formal Model of a Virtual Filesystem Switch

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.

Original Text (This is the original text for your reference.)

A Formal Model of a Virtual Filesystem Switch

+More

Keywords

formal model afs virtual filesystem switch verified file system linux directory tree component fuse

Cite this article

APA

MLA

Chicago

,.A Formal Model of a Virtual Filesystem Switch. 102 (Proc. SSV 2012),.

References

Disclaimer: The translated content is provided by third-party translation service providers, and IKCEST shall not assume any responsibility for the accuracy and legality of the content.