Trustworthy Systems

Device driver synthesis

Authors

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

Intel Corporation

NICTA

Abstract

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

  @article{Vij_KRHZRWL_13,
    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         = {https://trustworthy.systems/publications/nicta_full_text/7690.pdf},
    title            = {Device Driver Synthesis},
    volume           = {17},
    year             = {2013}
  }

Download