Termite: Automatic Synthesis of Device Drivers
Overview
In this project we explore a radically new approach to driver development. We believe that the conventional manual driver development methodology is redundant since all the knowledge required to control the device from software is created during the design of the device and hence a driver for the device can be derived automatically from hardware design artifacts.
The ultimate goal of Termite is to come up with an automatic driver synthesis methodology that will guarantee correctness by construction. As the first step in this direction we implemented a semi-automatic approach where the driver is synthesised based on a formal specification of the device. Such specification must be developed manually based on informal device documentation. More precisely, in order to synthesise a device driver one needs to provide three formal specifications: a device-class specification that describes common properties of a class of similar devices, a device specification that describes a concrete representative of the class, and an OS interface specification that describes the communication protocol between the driver and the OS. Given these specifications, the driver sytnthesis algorithm computes a state machine of the driver and translates it into a driver implementation in C.
Ongoing work on the project is focusing on generating device drivers based on the device testbench that is used by hardware designers to verify the correctness of the register-transfer-level (RTL) model of the device.
Our partners
- Our approach to driver synthesis will not work without cooperation from hardware vendors. Therefore we are pursuing this research in collaboration with the OS Research Group at Intel.
- We are a proud recipient of a Google Research Award. This award will enable us to put more manpower on the project and purchase equipment in 2010.
