Name
Abstract | ||
|---|---|---|
The verification of device drivers is essential for the pervasive verification of an oper- ating system. To show the correctness of device drivers, devices have to be formally modeled. In this paper we present the formal model of the serial interface controller UART 16550A. By com- bining the device model with a formal model of a processor instruction set architecture we obtain an assembler-level programming model for a serial interface. As a programming and verification example we present a simple UART driver implemented in assembler and prove its correctness. All models presented in this paper have been formally specified in the Isabelle/HOL theorem prover. |
Year | Venue | Keywords |
|---|---|---|
2007 | VERIFY | instruction set architecture,programming model,theorem prover |
Field | DocType | Citations |
HOL,Control theory,Programming language,Programming paradigm,Instruction set,Computer science,Correctness,Serial port,Universal asynchronous receiver/transmitter | Conference | 11 |
PageRank | References | Authors |
0.81 | 7 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eyad Alkassar | 1 | 266 | 22.49 |
| Mark A. Hillebrand | 2 | 200 | 15.17 |
| Steffen Knapp | 3 | 61 | 5.20 |
| Rostislav Rusev | 4 | 34 | 3.18 |
| Sergey Tverdyshev | 5 | 123 | 9.27 |