Simulating a flash file system with CoreASM and Eclipse
Abstract
The formal specification of a file system for flash memory is the first step towards its verification. But creating such a formal specification is complex and errorprone. Visualizing the system state and having an executable version of the specification helps to better understand the specified system. In this paper, we present an approach for simulating and visualizing specifications written in the Abstract State Machine (ASM) formalism. We extend the ASM execution engine CoreASM to execute ASMs written using algebraic specifications. Furthermore we develop an Eclipsebased visualization framework and integrate CoreASM into it. This enables us to create different abstract views of the CoreASM system state and allows the user to interact with the specification in an intuitive way. We apply our techniques to the visualization of an abstract specification of a flash memory file system and report on our experiences with CoreASM and Eclipse.
- Citation
- BibTeX
Junker, M., Haneberg, D., Schellhorn, G., Reif, W. & Ernst, G.,
(2011).
Simulating a flash file system with CoreASM and Eclipse.
In:
Heiß, H.-U., Pepper, P., Schlingloff, H. & Schneider, J.
(Hrsg.),
INFORMATIK 2011 – Informatik schafft Communities.
Bonn:
Gesellschaft für Informatik e.V..
(S. 355-355).
@inproceedings{mci/Junker2011,
author = {Junker, Maximilian AND Haneberg, Dominik AND Schellhorn, Gerhard AND Reif, Wolfgang AND Ernst, Gidon},
title = {Simulating a flash file system with CoreASM and Eclipse},
booktitle = {INFORMATIK 2011 – Informatik schafft Communities},
year = {2011},
editor = {Heiß, Hans-Ulrich AND Pepper, Peter AND Schlingloff, Holger AND Schneider, Jörg} ,
pages = { 355-355 },
publisher = {Gesellschaft für Informatik e.V.},
address = {Bonn}
}
author = {Junker, Maximilian AND Haneberg, Dominik AND Schellhorn, Gerhard AND Reif, Wolfgang AND Ernst, Gidon},
title = {Simulating a flash file system with CoreASM and Eclipse},
booktitle = {INFORMATIK 2011 – Informatik schafft Communities},
year = {2011},
editor = {Heiß, Hans-Ulrich AND Pepper, Peter AND Schlingloff, Holger AND Schneider, Jörg} ,
pages = { 355-355 },
publisher = {Gesellschaft für Informatik e.V.},
address = {Bonn}
}
Haben Sie fehlerhafte Angaben entdeckt? Sagen Sie uns Bescheid: Send Feedback
More Info
ISBN: 978-88579-286-4
ISSN: 1617-5468
xmlui.MetaDataDisplay.field.date: 2011
Language:
(en)

Content Type: Text/Conference Paper