Abstract Specification of the UBIFS File System for Flash Memory
Abstract Specification of the UBIFS File System for Flash Memory
复制标题
闪存UBIFS文件系统抽象规范
DOI：
10.1007/978-3-642-05089-3_13
复制
发表时间：
2009
影响因子：
1.2
通讯作者：
W. Reif
中科院分区：
文献类型：
--
作者：
A. Schierl;G. Schellhorn;Dominik Haneberg;W. Reif
今天，我们看到对闪存的需求不断增长，因为它具有某些优势，例如抵抗动力学冲击。但是，可靠的数据存储还需要一个专门的文件系统知道并处理闪存的局限性。本文为UBIFS Flash文件系统开发了一个正式的抽象模型，该模型最近已包含在Linux内核中。我们为文件系统的核心组件开发了正式的规格：基于Inode的文件存储，闪存索引，其在RAM中的缓存副本和日记帐中的副本，以节省差异。基于这些数据结构，我们对UBIF的接口操作进行抽象规范，并使用交互式验证系统KIV证明了一些最重要的属性。
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.