Trustworthy Systems

Device driver synthesis


Mona Vij, John Keys, Arun Raghunath, Scott Hahn, Vincent Zimmer, Leonid Ryzhyk, Adam Christopher Walker and Alexander Legg

Intel Corporation



Automatic Device Driver Synthesis is a research collaboration project between Intel and National Information Communications Technology Australia (NICTA) that aims to synthesize device drivers automatically using formal OS and device specifications. We have built a tool chain that uses Simics DML Device model sources as an input to the driver synthesis tool chain. The tool chain has a frontend compiler that extracts the device behavior from the Device Modeling Language (DML) model and outputs a formal representation of the device behavior that we refer to as a device specification. The driver synthesis tool combines this specification with a similar O/S specification and applies the principles of game theory to compute a winning strategy on behalf of the driver and eventually converts it into driver C code. This approach aims to use the existing device models for producing device drivers resulting in highly reliable drivers and faster time to market. We have synthesized a number of drivers using our tool chain. Some examples include legacy IDE controller, UART, SDHCI controller, and a minimal Ethernet adapter.

BibTeX Entry

    author           = {Vij, Mona and Keys, John and Raghunath, Arun and Hahn, Scott and Zimmer, Vincent and Ryzhyk, Leonid
                        and Walker, Adam Christopher and Legg, Alexander},
    isbn             = {978-1-934053-62-1},
    journal          = {Intel Technology Journal},
    keywords         = {device driver synthesis},
    month            = dec,
    number           = {2},
    pages            = {136--157},
    paperurl         = {},
    title            = {Device Driver Synthesis},
    volume           = {17},
    year             = {2013}