Temporal Specification Oriented Fuzzing for Trigger-Action-Programming Smart Home Integrations

The convergence of Internet of Things (IoT) and home automation (HA) has revolutionized human-device interaction, typically through trigger-action programming paradigms such as If This Then That (IFTTT). While empowering user-customized automation, this integration introduces critical challenges: unexpected behaviors from improper rule configurations, and cybersecurity threats propagated through interconnected rule chains. Researchers model the integrations with the finite state machine, characterize these risks using linear temporal logic (LTL), and employ model checking techniques to check whether the system conforms to the properties. However, model checking suffers from the inherent state space explosion problem, so that relevant methods face difficulty in handling large-scale systems. Furthermore, the HA-IoT domain notably lacks standardized benchmark datasets for validating LTL-related methods.