Inside a Verified Flash File System: Transactions and Garbage Collection
Inside a Verified Flash File System: Transactions and Garbage Collection
复制标题
在经过验证的闪存文件系统内部：事务和垃圾收集
DOI：
10.1007/978-3-319-29613-5_5
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
W. Reif
中科院分区：
文献类型：
--
作者：
G. Ernst;J. Pfähler;G. Schellhorn;W. Reif
这里提出的工作解决了闪存文件系统验证中的一个长期存在的概念差距：我们将一个抽象的基于图形的表示映射到存储介质的扁平字节块。具体来说，我们考虑分组的文件系统对象到原子事务连同布局，分配和垃圾收集的闪存存储空间。两个主要问题指导设计和验证：正确处理错误，更重要的是，保证从意外断电中恢复。找到有用的规范的中间接口，以解决这些问题实际上占主导地位的验证工作。
The work presented here addresses a long-standing conceptual gap in flash file system verification: We map an abstract graph-based representation down to the flat blocks of bytes of the storage medium. Specifically, we consider grouping of file system objects into atomic transactions together with layout, allocation and garbage collection of on-flash storage space. Two major concerns guide the design and verification: proper handling of errors and, more importantly, guaranteed recovery from unexpected power cuts. Findinguseful specificationsof intermediate interfaces to address these concerns realistically dominates the verification effort.
登录
查看更多内容
虚拟文件系统交换机的验证
DOI：
10.1007/978-3-642-54108-7_13
发表时间：
2013
期刊：
12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007)
影响因子：
--
作者：
G. Ernst;G. Schellhorn;Dominik Haneberg;J. Pfähler;W. Reif
通讯作者：
W. Reif
闪存UBIFS文件系统抽象规范
影响因子：
1.2
作者：
A. Schierl;G. Schellhorn;Dominik Haneberg;W. Reif
通讯作者：
W. Reif
一个小挑战：构建一个可验证的文件系统
影响因子：
1
作者：
Rajeev Joshi;G. Holzmann
通讯作者：
G. Holzmann
DOI：
10.1007/s10009-014-0308-3
发表时间：
2015-11-01
影响因子：
1.5
作者：
Ernst, Gidon;Pfaehler, Joerg;Reif, Wolfgang
通讯作者：
Reif, Wolfgang
公平 ASM 细化的完整性
DOI：
10.1016/j.scico.2009.10.004
发表时间：
2011
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
G. Schellhorn
通讯作者：
G. Schellhorn