Paper Info
Title
Abstract Specification of the UBIFS File System for Flash Memory
Abstract
Today we see an increasing demand for flash memory because it has certain advantages like resistance against kinetic shock. However, reliable data storage also requires a specialized file system knowing and handling the limitations of flash memory. This paper develops a formal, abstract model for the UBIFS flash file system, which has recently been included in the Linux kernel. We develop formal specifications for the core components of the file system: the inode-based file store, the flash index, its cached copy in the RAM and the journal to save the differences. Based on these data structures we give an abstract specification of the interface operations of UBIFS and prove some of the most important properties using the interactive verification system KIV.
Year
DOI
Venue
2009
10.1007/978-3-642-05089-3_13
FM
Keywords
Field
DocType
abstract specification,file system,specialized file system,abstract model,interactive verification system,flash index,flash memory,ubifs file system,inode-based file store,data structure,ubifs flash file system,kinetics,indexation,formal specification,data storage
JFFS2,File system,Flash file system,inode,Computer science,Flash memory emulator,Versioning file system,Memory-mapped file,Operating system,Computer file
Conference
Volume
ISSN
Citations 
5850
0302-9743
19
PageRank 
References 
Authors
1.15
22
4
Name
Order
Citations
PageRank
Andreas Schierl1358.19
Gerhard Schellhorn276956.43
Dominik Haneberg318213.37
Wolfgang Reif491595.46