Verification of a Virtual Filesystem Switch
Verification of a Virtual Filesystem Switch
复制标题
虚拟文件系统交换机的验证
DOI：
10.1007/978-3-642-54108-7_13
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
W. Reif
中科院分区：
文献类型：
--
作者：
G. Ernst;G. Schellhorn;Dominik Haneberg;J. Pfähler;W. Reif
这项工作介绍了我们验证的一部分工作，以构建正确的文件系统以用于闪存。作为蓝图，我们使用的是Linux的一部分的Ubifs。作为Linux中的所有文件系统，UBIFS实现了虚拟文件Switch VFS接口。 VF依次实施顶级POSIX操作。本文弥合了POSIX的抽象规范与ASM改进的VFS现象模型之间的差距。模型和证明是在交互式定理示意剂KIV中机械化的。使用分离逻辑将代数目录树映射到VF的指针结构。我们考虑使用硬链链接，文件处理和将文件内容分配到页面中。
This work presents part of our verification effort to construct a correct file system for Flash memory. As a blueprint we use UBIFS, which is part of Linux. As all file systems in Linux, UBIFS implements the Virtual Filesystem Switch VFS interface. VFS in turn implements top-level POSIX operations. This paper bridges the gap between an abstract specification of POSIX and a realistic model of VFS by ASM refinement. The models and proofs are mechanized in the interactive theorem prover KIV. Algebraic directory trees are mapped to the pointer structures of VFS using Separation Logic. We consider hard-links, file handles and the partitioning of file content into pages.