Sciweavers

EMSOFT
2007
Springer

Verification of device drivers and intelligent controllers: a case study

13 years 8 months ago
Verification of device drivers and intelligent controllers: a case study
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. Categor...
David Monniaux
Added 14 Aug 2010
Updated 14 Aug 2010
Type Conference
Year 2007
Where EMSOFT
Authors David Monniaux
Comments (0)