Model-Checking the Linux Virtual File System

摘要

This paper presents a case study in modelling and verifyingthe Linux Virtual File System (VFS). Our work is set in the context ofHoare's verification grand challenge and, in particular, Joshi and Holz-mann's mini-challenge to build a verifiable file system. The aim of thestudy is to assess the viability of retrospective verification of a VFSimplementation using model-checking technology. We show how to ex-tract an executable model of the Linux VFS implementation, validatethe model by employing the simulation capabilities of SPIN, and analyseit for adherence to data integrity constraints and deadlock freedom usingthe SMART model checker.