Model-Checking the Linux Virtual File System

Andy Galloway, Gerald Luettgen, Jan Tobias Muehlberg, Radu I. Siminiceanu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationVERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION
EditorsND Jones, M MullerOlm
Place of PublicationBERLIN
PublisherSpringer
Pages74-88
Number of pages15
Volume5403 LNCS
ISBN (Print)978-3-540-93899-6
Publication statusPublished - 2009
Event10th International Conference on Verification, Model Checking, and Abstract Interpretation - Savannah
Duration: 18 Jan 200920 Jan 2009

Conference

Conference10th International Conference on Verification, Model Checking, and Abstract Interpretation
CitySavannah
Period18/01/0920/01/09

Keywords

  • VERIFICATION
  • CHALLENGE

Cite this