Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1016/j.scico.2016.04.009 | Science of Computer Programming |
Keywords | Field | DocType |
Abstract State Machine,Refinement,Flash file systems,Crash safety,Power cuts | Crash,Programming language,Flash file system,Computer science,Abstract state machines,Theoretical computer science,Modular design,Semantics | Journal |
Volume | ISSN | Citations |
131 | 0167-6423 | 2 |
PageRank | References | Authors |
0.37 | 25 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gidon Ernst | 1 | 144 | 14.46 |
| Jörg Pfähler | 2 | 82 | 6.28 |
| Gerhard Schellhorn | 3 | 769 | 56.43 |
| Wolfgang Reif | 4 | 64 | 4.83 |