Modular, crash-safe refinement for ASMs with submachines
Modular, crash-safe refinement for ASMs with submachines
复制标题
带有子机的 ASM 的模块化、防碰撞改进
DOI：
10.1016/j.scico.2016.04.009
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
W. Reif
中科院分区：
文献类型：
--
作者：
G. Ernst;J. Pfähler;G. Schellhorn;W. Reif
在本文中，我们定义了一个正式的细化理论的一个变种的抽象状态机（ASMs）与子机和断电。该理论的动机是一个经过验证的闪存文件系统的发展。系统的不同组件被建模为子机，并单独细化。我们定义了一个非原子的语义，是适合考虑在操作中断电。我们证明了细化是组成方面的submachines和崩溃。我们给出了一个标准“崩溃中立性”和相应的证明义务，足以减少非原子推理标准的前/后验证的文件系统中的电源故障的情况下。
In this paper we define a formal refinement theory for a variant of Abstract State Machines (ASMs) with submachines and power cuts. The theory is motivated by the development of a verified flash file system. Different components of the system are modeled as submachines and refined individually. We define a non-atomic semantics that is suitable for considering power cuts in the middle of operations. We prove that refinement is compositional with respect to submachines and crashes. We give a criterion “crash-neutrality” and corresponding proof obligations that are sufficient to reduce non-atomic reasoning to standard pre/post verification in the context of power failures in file systems.
登录
查看更多内容
指定实际的文件系统
DOI：
--
发表时间：
2015
期刊：
MARS
影响因子：
--
作者：
Sidney Amani;Toby C. Murray
通讯作者：
Toby C. Murray
虚拟文件系统交换机的验证
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
一个小挑战：构建一个可验证的文件系统
影响因子：
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