Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

INFORMATIK 2011 Informatik schafft Communities P-192, 355-355 (2011).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


Reif, gidon ernst simulating a flash file system with coreasm and eclipse

Dominik Haneberg , Maximilian Junker , Gerhard Schellhorn and Wolfgang


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.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-88579-286-4

Last changed 21.02.2014 20:08:11