Linux Device Driver Synthesis and Verification

Abstract

The device driver is a program which provides a software interface to a hardware device, enabling operating systems and other computer programs to access hardware functions without needing to know the details of the hardware. Recently, aggressive scaling of complex hardware and software components make the device driver development process cumbersome and error prone. This disadvantage creates an incentive for people to seek an automatic and robust approach of the device driver synthesis. This thesis is concerned with integrating a formal method verification into the driver synthesis process, and we make the following contributions. First, we present an approach to automatic driver synthesis based on model-integrated computing. Second, we define a formal graphic domain specific language for specifying a device driver model and its environment. Third, by using the abstract state machine of a driver model as an intermediate representation, we apply model-checking techniques to eliminate errors introduced during manual abstraction and verify that the resulting device driver constitutes a reliable device behavior.