Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2003: Formal Methods and Software Engineering pp 599–619Cite as

A Formal Model for the Block Device Subsystem of the Linux Kernel

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2885))

Abstract

A formal model of the block-device subsystem of the Linux operating system kernel is set out here, as an introduction to the kernel for formal methods people and a preliminary to further formal methods work. The model is abstract, but executable, and it is faithful to the detail of the real Linux kernel code. The model is used here to analyse kernel behavior. It is proved of the model that the kernel block device system cannot deadlock.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Breuer, P.T., Marín Lopez, A., García, A.: The Network Block Device. The Linux Journal #73 (September 2002), http://www2.linuxjournal.com/lj-issues/issue73/3778.html

  2. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM Symposium on the Principles of Programming Languages, pp. 238–252 (1977)

    Google Scholar 

  3. Jones, M.P.: Introduction to Gofer. Technical report, Department of Computer Science, Yale University, USA (September 1991) ( part of the Gofer distribution, anonymous ftp from ftp.cs.nott.ac.uk in the directory nott-fp/languages/gofer, rev. October 1994)

  4. Raymond, E.S.: The Cathedral and the Bazaar Linux Kongress (May 1997), http://www.tuxedo.org/~sr/writings/cathedral-bazaar/cathedral-bazaar/

  5. Rubini, A.: Linux Device Drivers. O’Reilly, Sebastopol (February 1998)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Carlos III de Madrid,  

    Peter T. Breuer

Authors
  1. Peter T. Breuer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, National University of Singapore, Singapore

    Jin Song Dong

  2. University of York,  

    Jim Woodcock

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Breuer, P.T. (2003). A Formal Model for the Block Device Subsystem of the Linux Kernel. In: Dong, J.S., Woodcock, J. (eds) Formal Methods and Software Engineering. ICFEM 2003. Lecture Notes in Computer Science, vol 2885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39893-6_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39893-6_34

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20461-9

  • Online ISBN: 978-3-540-39893-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation