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...

• Type: Conference
• Year: 2007
• Where: EMSOFT
• Authors: David Monniaux
• Keywords: Device Driver, Direct Memory, EMSOFT 2007, Perform Direct Memory, Software Engineering