Verification of Device Drivers and Intelligent Controllers: a Case StudyReportar como inadecuado

Verification of Device Drivers and Intelligent Controllers: a Case Study - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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

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

Keywords : Device driver verification USB OHCI asynchronous direct memory access linked lists parallelism

Autor: David Monniaux -



Documentos relacionados