Automatic Verification of Active Device Drivers

Select |




Print


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

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


2014-01


Journal Article


Operating Systems Review


48


1


106-108


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


Dingo, device drivers, verification


https://doi.org/10.1145/2626401.2626424


© ACM, 2017. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Operating Systems Review , {VOL48, ISS1, (Jan 2014)} http://doi.acm.org/10.1145/2626401.2626424


Published Version (pdf) (305KB)


English


nicta:8142


Amani, Sidney; Chubb, Peter; Donaldson, Alastair; Legg, Alexander; Ong, Keng Chai; Ryzhyk, Leonid; Zhu, Yanjin. Automatic Verification of Active Device Drivers . Operating Systems Review. 2014-01; 48(1):106-108. https://doi.org/10.1145/2626401.2626424



Loading citation data...

Citation counts
(Requires subscription to view)