Simulating a Flash File System with CoreASM and Eclipse
Maximilian Junker, Dominik Haneberg, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst · OPUS (Augsburg University) · 2011
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 error- prone. Visualizing the system state and having an executable version of the specifi- cation 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 exe- cute ASMs written using algebraic specifications. Furthermore we develop an Eclipse- based visualization framework and integrate CoreASM into it. This enables us to cre- ate 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.