Correctness Proofs for Device Drivers in Embedded Systems
Computer systems do not exist in isolation: they must interact with the world through I/O devices. The authors' work, which focuses on constrained embedded systems, provides a framework for verifying device driver software at the machine code level. The authors created an abstract device model that can be plugged into an existing formal semantics for an instruction set architecture. They have instantiated the abstract model with a model for the serial port for a real embedded processor, and they have verified the full functional correctness of the transmit and receive functions from an open-source driver for this device.