Verification of Device Drivers and Intelligent Controllers: a Case Study

David Monniaux (1)

1 LIENS - Laboratoire d'informatique de l'école normale supérieure

The soundness of device drivers generally cannot be verified in isolation, but has to take into account the reactions of the hardware devices. In critical embedded systems, interfaces often were simple "volatile" variables, and the interface specification typically a list of bounds on these variables. Some newer systems use "intelligent" controllers that handle dynamic worklists in shared memory and perform direct memory accesses, all asynchronously from the main processor. Thus, it is impossible to truly verify the device driver without taking the intelligent device into account, because incorrect programming of the device can lead to dire consequences, such as memory zones being erased. We have successfully verified a device driver extracted from a critical industrial system, asynchronously combined with a model for a USB OHCI controller. This paper studies this case, as well as introduces a model and analysis techniques for this asynchronous composition.

Mots clés: Device driver; verification; USB; OHCI; asynchronous; direct memory access; linked lists; parallelism

Domaines: Langage de programmation [cs.PL]; Systèmes embarqués; Système d'exploitation [cs.OS]; Génie logiciel [cs.SE]

David Monniaux. Verification of Device Drivers and Intelligent Controllers: a Case Study. International Conference On Embedded Software (EMSOFT), Sep 2007, Salzburg, Austria. pp.30 - 36, ⟨10.1145/1289927.1289937⟩. ⟨hal-00158869⟩