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.