Using Model Checking to Debug Device Firmware