Title: Formal Modeling and Analysis of a Flash Filesystem in Alloy

Speaker:  Eunsuk Kang

Place: 	32-G531
Time: 	1-2:30pm
Date: 	Friday, March 14, 2008
 
Abstract: In this talk, I will present recent work in the formal modeling and analysis of
a design for a flash-based filesystem in Alloy.  We model the basic operations of a
filesystem as well as features that are crucial to NAND flash hardware, such as
wear-leveling and erase-unit reclamation.  In addition, we address the issue of fault
tolerance by modeling a mechanism for recovery from interrupted filesystem operations due
to an unexpected power loss.  We analyze the correctness of our flash filesystem model by
checking trace inclusion against a POSIX-compliant abstract filesystem, in which a file
is modeled simply as an array of data elements.  The analysis in Alloy is fully automatic
and complete within a finite scope.    This work was in part motivated by the NASA Mars
Exploration Rovers, one of which suffered a major system failure in 2004 due to a flaw in
the on-board flash filesystem.