Bug-Free Sensors: The Automatic Verification of Context-Aware TinyOS Applications