Publikation
Formal Functional Verification of Device Drivers
Eyad Alkassar; Mark Hillebrand
In: Jim Woodcock; Natarajan Shankar (Hrsg.). Verified Software: Theories, Tools, Experiments. International Conference on Verified Software: Theories, Tools, Experiments (VSTTE-08), Second International Conference, October 6-9, Toronto, ON, Canada, Pages 225-239, Lecture Notes in Computer Science (LNCS), Vol. 5295, ISBN 978-3-540-87872-8, Springer, 2008.
Zusammenfassung
We report on the formal functional verification of a simple device driver for an ATAPI hard disk in Isabelle/HOL. The proof is based on a functional model of the hard disk, which has been integrated into the instruction set architecture of a verified RISC processor as one of several memory-mapped devices. The result is an interleaved computational model, in which the devices and the processor take turns in execution. Even in this concurrent context, the verification can be kept largely sequential and modular with respect to the other devices. This is made possible by sound reordering of computation traces, given that devices do not interfere with each other and the driver monopolizes the hard disk. To the best of our knowledge, this paper presents the first formal functional verification of a device driver against a realistic device and system model.