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.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Eyad Alkassar, Mark A. Hillebrand, Steffen Knapp, Rostislav Rusev, Sergey Tverdyshev
• Keywords: Automated Reasoning, CADE 2007, Formal Model, Interface Controller Uart, Simple Uart Driver