Model-Checking the Linux Virtual File System

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

Model-Checking the Linux Virtual File System

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION
Editors	ND Jones, M MullerOlm
Place of Publication	BERLIN
Publisher	Springer
Pages	74-88
Number of pages	15
Volume	5403 LNCS
ISBN (Print)	978-3-540-93899-6
Publication status	Published - 2009
Event	10th International Conference on Verification, Model Checking, and Abstract Interpretation - Savannah Duration: 18 Jan 2009 → 20 Jan 2009

Conference

Conference	10th International Conference on Verification, Model Checking, and Abstract Interpretation
City	Savannah
Period	18/01/09 → 20/01/09

Keywords

VERIFICATION
CHALLENGE

Cite this

@inproceedings{339d911e7a8747328aef35bbea72c174,

title = "Model-Checking the Linux Virtual File System",

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.",

keywords = "VERIFICATION, CHALLENGE",

author = "Andy Galloway and Gerald Luettgen and Muehlberg, {Jan Tobias} and Siminiceanu, {Radu I.}",

year = "2009",

language = "English",

isbn = "978-3-540-93899-6",

volume = "5403 LNCS",

pages = "74--88",

editor = "ND Jones and M MullerOlm",

booktitle = "VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION",

publisher = "Springer",

address = "Germany",

note = "10th International Conference on Verification, Model Checking, and Abstract Interpretation ; Conference date: 18-01-2009 Through 20-01-2009",

}

TY - GEN

T1 - Model-Checking the Linux Virtual File System

AU - Galloway, Andy

AU - Luettgen, Gerald

AU - Muehlberg, Jan Tobias

AU - Siminiceanu, Radu I.

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - VERIFICATION

KW - CHALLENGE

UR - http://www.scopus.com/inward/record.url?scp=58449127569&partnerID=8YFLogxK

M3 - Conference contribution

SN - 978-3-540-93899-6

VL - 5403 LNCS

SP - 74

EP - 88

BT - VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION

A2 - Jones, ND

A2 - MullerOlm, M

PB - Springer

CY - BERLIN

T2 - 10th International Conference on Verification, Model Checking, and Abstract Interpretation

Y2 - 18 January 2009 through 20 January 2009

ER -

Model-Checking the Linux Virtual File System

Abstract

Conference

Keywords

Other files and links

Cite this