A joint project of the Graduate School, Peabody College, and the Jean & Alexander Heard Library

Title page for ETD etd-11172015-221551

Type of Document Master's Thesis
Author Li, Yi
Author's Email Address yi.li@vanderbilt.edu
URN etd-11172015-221551
Title Linux Device Driver Synthesis and Verification
Degree Master of Science
Department Computer Science
Advisory Committee
Advisor Name Title
Theodore Bapty Committee Chair
Sandeep Neema Committee Member
  • driver synthesis
  • model checking
  • domain specific language
Date of Defense 2015-08-21
Availability unrestricted
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.

  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  YiLi.pdf 1.06 Mb 00:04:55 00:02:31 00:02:12 00:01:06 00:00:05

Browse All Available ETDs by ( Author | Department )

If you have more questions or technical problems, please Contact LITS.