ISSE

Search

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


BibTex

The final publication is available at Elsevier via http://dx.doi.org/10.1016/j.scico.2016.04.009.

For questions regarding the publication, please contact publications@isse.de!


Downloads: