Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Experiences with Formal Specification of Fault-tolerant File Systems

Roxana Geambasu, Andrew Birrell, and John MacCormick


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.


Publication typeInproceedings
Published inProceedings of the 38th Annual International Conference on Dependable Systems and Networks
AddressAnchorage, Alaska
> Publications > Experiences with Formal Specification of Fault-tolerant File Systems