Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Towards Verifiable Device Drivers: An Approach based on Domain-Specific Languages

Abstract : Although peripheral devices come out at a frantic pace and require fast releases of drivers, little progress has been made to improve the development of drivers. Too often, this development consists of decoding hardware intricacies, based on ambiguous or incomplete documentation, to determine how to operate a device. Then, assembly-level operations need to be used to interact with the device. These low-level operations make the device driver fairly unreadable and prevent safety properties from being checked. This paper presents a language, named Devil, dedicated to defining the functional interface of a device. More precisely, Devil aims at specifying the access mechanisms, the type and layout of data, and behavioral properties involved in operating a device. The benefit of our approach is that, once compiled, a Devil description implements an interface which models an idealized device and abstracts the hardware intricacies. Unlike a general-purp- ose language, Devil allows a description to be thoroughly verified; this verification greatly improves the safety of the communications with the device. The design of Devil is based on key concepts we identified in analyzing the domain of device drivers. Our language has been used to specify a large number of PC devices including Ethernet, video, sound, interrupt, DMA and mouse controllers.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 11:05:36 AM
Last modification on : Wednesday, October 26, 2022 - 8:16:15 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:28:55 PM


  • HAL Id : inria-00072849, version 1



Fabrice Mérillon, Laurent Réveillère, Charles Consel, Robin Hansen, Renaud Marlet, et al.. Towards Verifiable Device Drivers: An Approach based on Domain-Specific Languages. [Research Report] RR-3809, INRIA. 1999. ⟨inria-00072849⟩



Record views


Files downloads