Sciweavers

Share
DSN
2008
IEEE

Experiences with formal specification of fault-tolerant file systems

8 years 5 months ago
Experiences with formal specification of fault-tolerant file systems
Fault-tolerant, replicated file systems are a crucial component of today's data centers. Despite their huge complexity, these systems are typically specified only in brief prose, which makes them difficult to reason about or verify. This paper describes the authors' experience using formal methods to improve our understanding of and confidence in the behavior of replicated file systems. We wrote formal specifications for three real-world fault-tolerant file systems and used them to: (1) expose design similarities and differences; (2) clarify and mechanically verify consistency properties; and (3) evaluate design alternatives. Our experience showed that formal specifications for these systems were easy to produce, useful for a deep understanding of system functions, and valuable for system comparison.
Roxana Geambasu, Andrew Birrell, John MacCormick
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where DSN
Authors Roxana Geambasu, Andrew Birrell, John MacCormick
Comments (0)
books