Using Model Checking to Debug Device Firmware

10 years 7 days ago
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...
Sanjeev Kumar, Kai Li
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2002
Where OSDI
Authors Sanjeev Kumar, Kai Li
Comments (0)