Sciweavers

Share
CADE
2007
Springer

Formal Device and Programming Model for a Serial Interface

12 years 7 days ago
Formal Device and Programming Model for a Serial Interface
Abstract. The verification of device drivers is essential for the pervasive verification of an operating 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 combining 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.
Eyad Alkassar, Mark A. Hillebrand, Steffen Knapp,
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Eyad Alkassar, Mark A. Hillebrand, Steffen Knapp, Rostislav Rusev, Sergey Tverdyshev
Comments (0)
books