Device driver synthesis and verification
The Device Driver is a program which allows the software or higher-level computer programs to interact with a hardware device. These software components which act as a glue between devices and operating systems, communicating with each of these systems and executing commands. They provide an abstraction layer for the software above and also a mediate the communication between the operating system kernel and the devices below.
Usually the operating system comes with a support for common device drivers and also the hardware vendors provide device driver for their hardware devices on most platforms. The aggressive scaling of the hardware devices and the complex software components has made the device driver development process cumbersome and complex. When the size and functionality of the drivers started increasing the device drivers became a key role in defining the reliability of the system. This has given a strong urge towards automatic synthesis and verification of device drivers. This survey shed some light in to the recent approaches in synthesis and verification of device drivers.
Motivation for automatic driver synthesis and verification
The device drivers are the principal failing component in most systems. The Berkeley Open Infrastructure for network Computing (BOINC) project found that OS crashes are predominantly caused by poorly-written device driver code . [1]. In Windows XP, drivers account for 85% of the reported failures. In the Linux kernel 2.4.1 device driver code accounts for about 70% of the code size [2]. The driver fault can crash the whole system as it is running in the kernel mode. These findings resulted in various methodologies and techniques for verification of device drivers. An alternative was to develop techniques which can synthesize device drivers robustly. Less human interaction in the development process and proper specification of the device and operating systems can lead to more reliable drivers.
The other motivation for driver synthesis was the increased number of flavors of operating system available. Each of these have its own set of input output control and specifications which makes support of hardware devices on each of the operating systems difficult. So ability to use a device with an operating system requires the availability of corresponding device driver combination. Hardware vendors supply the drivers for mostly windows, Linux and Mac Os but due to the high development or porting costs and technical support difficulties they are unable to provide drivers on all platforms. The automated synthesis can help the vendors in providing drivers to support any devices on any operating system.