Modular, Crash-Safe Refinement for ASMs with Submachines

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif

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.
published 2016 Science of Computer Programming

Publisher: Elsevier


The final publication is available at Elsevier via

For questions regarding the publication, please contact!