Formalizing a Hierarchical File System

In this note, we define an abstract file system as a partial function from (absolute) paths to data. Such a file system determines the set of valid paths. It allows the file system to be read and written at a valid path, and it allows the system to be modified by the Unix operations for removal (rm)...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2009-12, Vol.259, p.67-85
Main Authors: Hesselink, Wim H., Lali, M.I.
Format: Article
Language:English
Subjects:
File System
Permission System
Refinement
Specification
Theorem Proving
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this note, we define an abstract file system as a partial function from (absolute) paths to data. Such a file system determines the set of valid paths. It allows the file system to be read and written at a valid path, and it allows the system to be modified by the Unix operations for removal (rm), making of directories (mkdir), and moving (mv). We present abstract definitions (axioms) for these operations. This specification is refined towards a pointer implementation. To mitigate the problems attached to partial functions, we do this in two steps. First a refinement towards a pointer implementation with total functions, followed by one that allows partial functions. These two refinements are proved correct by means of a number of invariants. Indeed, the insight gained mainly consists of the invariants of the pointer implementation that are needed for the refinement functions. Finally, each of the three specification levels is enriched with a permission system for reading, writing, or executing, and the refinement relations between these permission systems are explored.
ISSN:1571-0661
1571-0661
DOI:10.1016/j.entcs.2009.12.018