Sciweavers

VMCAI
2009
Springer

Model-Checking the Linux Virtual File System

13 years 10 months ago
Model-Checking the Linux Virtual File System
This paper presents a case study in modelling and verifying the Linux Virtual File System (VFS). Our work is set in the context of Hoare’s verification grand challenge and, in particular, Joshi and Holzmann’s mini-challenge to build a verifiable file system. The aim of the study is to assess the viability of retrospective verification of a VFS implementation using model-checking technology. We show how to extract an executable model of the Linux VFS implementation, validate the model by employing the simulation capabilities of SPIN, and analyse it for adherence to data integrity constraints and deadlock freedom using the SMART model checker.
Andy Galloway, Gerald Lüttgen, Jan Tobias M&u
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where VMCAI
Authors Andy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg, Radu Siminiceanu
Comments (0)