Jason Croft, Ratul Mahajan, Matthew Caesar, and Madan Musuvathi
Networked devices such as locks and thermostats are now cheaply available, which is accelerating the adoption of home automation. But unintended behaviors of programs that control automated homes can pose severe problems, including security risks (e.g., accidental disarming of alarms). We facilitate predictable control of automated homes by letting users “fast forward” their program and observe its possible future behaviors under different sequences of inputs and environmental conditions. A key challenge that we face, which is not addressed by existing program exploration techniques, is to systematically handle time because home automation programs depend intimately on absolute and relative timing of inputs. We develop an approach that models programs as timed automata and incorporates novel mechanisms to enable scalable and comprehensive exploration of their behavior. We implement our approach in a tool called DeLorean and apply it to 10 real home automation programs. We find that it can fast forward these programs 3.6 times to 36K times faster than real time and uncover unintended behaviors in them.