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.
keyword : DSLS DEVICE DRIVERS
Type de document :
Rapport
[Research Report] RR-3809, INRIA. 1999
Liste complète des métadonnées

https://hal.inria.fr/inria-00072849
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 11:05:36
Dernière modification le : vendredi 6 avril 2018 - 13:42:02
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:28:55

Fichiers

Identifiants

  • HAL Id : inria-00072849, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

405

Téléchargements de fichiers

246