Formalizing a hierarchical file system

Wim H. Hesselink*, Muhammad Ikram Lali

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

10 Citations (Scopus)
304 Downloads (Pure)

Abstract

An abstract file system is defined here 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 creation, removal, and moving of files and directories. We present abstract definitions (axioms) for these operations. This specification is refined towards a pointer implementation. The challenge is to have a natural abstraction function from the implementation to the specification, to define operations on the concrete store that behave exactly in the same way as the corresponding functions on the abstract store, and to prove these facts. 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 insights gained consist, on the one hand, of the invariants of the pointer implementation that are needed for the refinement functions, and on the other hand of the precise enabling conditions of the operations on the different levels of abstraction. 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. Files and directories are distinguished from the outset, but this rarely affects our part of the specifications. All results have been verified with the proof assistant PVS, in particular, that the invariants are preserved by the operations, and that, where the invariants hold, the operations commute with the refinement functions.

Original languageEnglish
Pages (from-to)27-44
Number of pages18
JournalFormal Aspects of Computing
Volume24
Issue number1
DOIs
Publication statusPublished - Jan-2012

Keywords

  • File system
  • Specification
  • Verification
  • Refinement
  • Permission system
  • Theorem proving
  • MODEL CHECKING
  • FLASH MEMORY
  • SPECIFICATION
  • STORE

Fingerprint

Dive into the research topics of 'Formalizing a hierarchical file system'. Together they form a unique fingerprint.

Cite this