Using Model Checking to Debug Device Firmware

Device firmware is a piece of concurrent software that achieves high performance at the cost of software complexity. They contain subtle race conditions that make them difficult to debug using traditional debugging techniques. The problem is further compounded by the lack of debugging support on the devices. This is a serious problem because the device firmware is trusted by the operating system. Model checkers are designed to systematically verify properties of concurrent systems. Therefore, model checking is a promising approach to debugging device firmware. However, model checking involves an exponential search. Consequently, the models have to be small to allow effective model checking. er describes the abstraction techniques used by compiler to extract abstract models from device firmware written in ESP. The abstract models are small because they discard some of the details in the firmware that is irrelevant to the particular property being verified. The programmer is required to...

• Type: Conference
• Year: 2002
• Where: OSDI
• Authors: Sanjeev Kumar, Kai Li
• Keywords: Abstract Models, Device Firmware, Model Checking, Operating System, OSDI 2002