Trustworthy Systems

Formalising device driver interfaces


Leonid Ryzhyk, Ihor Kuz and Gernot Heiser



Open Kernel Labs


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

    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         = {},
    title            = {Formalising device driver interfaces},
    year             = {2007}