Name
Abstract | ||
|---|---|---|
We argue that the device driver architecture enforced by current operating systems complicates both manual and automatic reasoning about driver behaviour. In particular, it makes it hard and in some cases impossible to statically verify that the driver correctly interacts with the rest of the kernel. This limitation cannot be addressed solely via better verification tools. We maintain that qualitative improvement in the effectiveness of static driver verification must rely on an improved driver architecture, leading to drivers that are easier to write, understand, and verify. To support our claims, we present a device driver architecture, called active drivers, that satisfies these requirements. We outline our methodology for specifying and verifying active driver protocols using existing model checking tools and describe initial experimental results. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/2103799.2103809 | ApSys |
Keywords | Field | DocType |
device driver architecture,static driver verification,current operating system,improved driver architecture,automatic reasoning,driver behaviour,active driver protocol,better verification tool,existing model checking tool,active driver,static analysis,synchronization,model checking,reliability,satisfiability,operating system,message passing | Kernel (linear algebra),Synchronization,Architecture,Model checking,Computer science,Static analysis,Message passing,Embedded system | Conference |
Citations | PageRank | References |
5 | 0.45 | 9 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sidney Amani | 1 | 67 | 5.00 |
| Leonid Ryzhyk | 2 | 212 | 16.05 |
| Alastair F. Donaldson | 3 | 661 | 52.35 |
| Gernot Heiser | 4 | 2525 | 137.42 |
| Alexander Legg | 5 | 24 | 3.17 |
| Yanjin Zhu | 6 | 19 | 1.68 |