Active Device Drivers

Select |




Print


Amani, Sidney; Chubb, Peter; Donaldson, Alastair; Legg, Alexander; Ryzhyk, Leonid; Zhu, Yanjin

Amani, Sidney; Chubb, Peter; Donaldson, Alastair; Legg, Alexander; Ryzhyk, Leonid; Zhu, Yanjin


2012-09-23


Report


Sydney, Australia


We develop a practical solution to the problem of automatic verification of the interface between device drivers and the operating system. Our solution relies on a combination of improved driver architecture and verification tools. Unlike previous proposals for verification-friendly drivers, our driver development and verification methodology supports drivers written in C and can be implemented in any existing OS. Our Linux-based evaluation shows that this methodology amplifies the power of existing model checking tools in detecting driver bugs, making it possible to verify properties that are beyond the reach of traditional techniques.


device drivers, reliability, model checking


1833-9646-6317


nicta:6317


Amani, Sidney; Chubb, Peter; Donaldson, Alastair; Legg, Alexander; Ryzhyk, Leonid; Zhu, Yanjin. Active Device Drivers. 2012-09-23. nicta:6317.



Loading citation data...

Citation counts
(Requires subscription to view)