A Formal Model of a Virtual Filesystem Switch

A Formal Model of a Virtual Filesystem Switch

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 operatio...

Full description

Bibliographic Details
Main Authors: Jörg Pfähler, Wolfgang Reif, Dominik Haneberg, Gerhard Schellhorn, Gidon Ernst
Format: Article
Language:English
Published: Open Publishing Association 2012-11-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1211.6187v1
id doaj-4256a88d0172485584e3d60cd6c1e0fc
record_format Article
spelling doaj-4256a88d0172485584e3d60cd6c1e0fc2020-11-24T23:23:59ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-11-01102Proc. SSV 2012334510.4204/EPTCS.102.5A Formal Model of a Virtual Filesystem SwitchJörg PfählerWolfgang ReifDominik HanebergGerhard SchellhornGidon ErnstThis 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.http://arxiv.org/pdf/1211.6187v1
collection DOAJ
language English
format Article
sources DOAJ
author Jörg Pfähler
Wolfgang Reif
Dominik Haneberg
Gerhard Schellhorn
Gidon Ernst
spellingShingle Jörg Pfähler
Wolfgang Reif
Dominik Haneberg
Gerhard Schellhorn
Gidon Ernst
A Formal Model of a Virtual Filesystem Switch
Electronic Proceedings in Theoretical Computer Science
author_facet Jörg Pfähler
Wolfgang Reif
Dominik Haneberg
Gerhard Schellhorn
Gidon Ernst
author_sort Jörg Pfähler
title A Formal Model of a Virtual Filesystem Switch
title_short A Formal Model of a Virtual Filesystem Switch
title_full A Formal Model of a Virtual Filesystem Switch
title_fullStr A Formal Model of a Virtual Filesystem Switch
title_full_unstemmed A Formal Model of a Virtual Filesystem Switch
title_sort formal model of a virtual filesystem switch
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2012-11-01
description 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.
url http://arxiv.org/pdf/1211.6187v1
work_keys_str_mv AT jorgpfahler aformalmodelofavirtualfilesystemswitch
AT wolfgangreif aformalmodelofavirtualfilesystemswitch
AT dominikhaneberg aformalmodelofavirtualfilesystemswitch
AT gerhardschellhorn aformalmodelofavirtualfilesystemswitch
AT gidonernst aformalmodelofavirtualfilesystemswitch
AT jorgpfahler formalmodelofavirtualfilesystemswitch
AT wolfgangreif formalmodelofavirtualfilesystemswitch
AT dominikhaneberg formalmodelofavirtualfilesystemswitch
AT gerhardschellhorn formalmodelofavirtualfilesystemswitch
AT gidonernst formalmodelofavirtualfilesystemswitch
_version_ 1725562523513520128

Similar Items