一句话：提出面向 LTL 时序规约的模糊测试方法，规避模型检测的状态爆炸，发现智能家居触发-动作集成中的规则缺陷与安全风险。
IoT 与家庭自动化的融合催生了 IFTTT 等触发-动作编程（TAP）范式，用户可自定义自动化规则。但不合理的规则配置会引发意外行为，互联的规则链还会传播网络安全威胁。已有研究用有限状态机建模 TAP 集成、以线性时序逻辑（LTL）刻画风险，并用模型检测验证系统是否满足性质；然而模型检测存在固有的状态空间爆炸问题，难以处理大规模系统，且该领域缺少用于验证 LTL 相关方法的标准基准数据集。本文提出面向时序规约的模糊测试方法，以 LTL 性质为导向驱动测试执行，暴露违反时序规约的行为，绕开完整状态空间枚举带来的可扩展性瓶颈，并针对基准数据缺失问题给出应对。
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.
@inproceedings{paperbot11560,
title = {Temporal Specification Oriented Fuzzing for Trigger-Action-Programming Smart Home Integrations},
author = {Jinglin Dai and Yifan Xiong and Lezhi Ma and Shangqing Liu and Lei Bu},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3764543}
}