Show simple item record

Linux Device Driver Synthesis and Verification

dc.creatorLi, Yi
dc.description.abstractThe 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.
dc.subjectdriver synthesis
dc.subjectmodel checking
dc.subjectdomain specific language
dc.titleLinux Device Driver Synthesis and Verification
dc.contributor.committeeMemberSandeep Neema
dc.type.materialtext Science University
dc.contributor.committeeChairTheodore Bapty

Files in this item


This item appears in the following Collection(s)

Show simple item record