Trustworthy Systems

Formalising device driver interfaces

Authors

Leonid Ryzhyk, Ihor Kuz and Gernot Heiser

NICTA

UNSW

Open Kernel Labs

Abstract

The lack of well-defined protocols for interaction with the operating system is a common source of defects in device drivers. In this paper we investigate the use of a formal language to define these protocols unambiguously. We present a language that allows us to convey all important requirements for driver behaviour in a compact specification and that can be readily understood by software engineers. It is intended to close the communication gap between OS and driver developers and enable more reliable device drivers.

BibTeX Entry

  @inproceedings{Ryzhyk_KH_07,
    address          = {Stevenson, WA, USA},
    author           = {Ryzhyk, Leonid and Kuz, Ihor and Heiser, Gernot},
    booktitle        = {Workshop on Programming Languages and Operating Systems (PLOS)},
    keywords         = {os, device driver, formalisation},
    month            = oct,
    pages            = {5},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/494.pdf},
    title            = {Formalising device driver interfaces},
    year             = {2007}
  }

Download