Systematically Ensuring the Confidence of Real-Time Home Automation IoT Systems
Systematically Ensuring the Confidence of Real-Time Home Automation IoT Systems
复制标题
系统地确保实时家庭自动化物联网系统的可信度
DOI：
10.1145/3185501
复制
发表时间：
2018-06
期刊：
影响因子：
--
通讯作者：
ong Li
中科院分区：
文献类型：
--
作者：
Lei Bu;Wen Xiong;Mike Liang;Shi Han;Dongmei Zhang;SHan Lin;Xu;ong Li
物联网 (IoT) 的最新进展和行业标准加速了联网设备在现实世界中的采用。为了管理这种数字实时设备和模拟环境的混合系统，业界推出了几种流行的家庭自动化物联网 (HA-IoT) 框架，例如 If-This-Then-That (IFTTT)、Apple HomeKit 和 Google Brillo。通常，用户通过指定触发传感器事件和触发的设备命令来创作设备交互。在这个看似简单的软件系统中，两个主导因素控制着系统相对于物理世界的置信属性。首先，物联网用户大多是非专家，缺乏对潜在影响以及与现有规则的共同影响的综合考虑。其次，虽然物联网设备日益复杂，可以对连续实时环境进行细粒度控制（例如加热器温度），但即使是两个简单连接的设备也可以有巨大的状态空间可供探索。事实上，错误控制设备和家用电器的错误可能会对系统正确性甚至用户人身安全产生影响。帮助用户确保他们创建的系统满足他们的期望至关重要。在本文中，我们介绍了如何实际应用混合自动机技术来帮助非专业物联网用户对此类混合 HA-IoT 系统进行置信度检查。我们提出了一个用于端到端编程帮助的自动化框架。我们自动构建并检查系统的线性混合自动机（LHA）模型。我们还提出了一种基于量词消除的方法来分析找到的反例并综合修复建议。我们基于这个框架和提出的技术实现了一个平台，MenShen。我们对多达 46 台设备和 65 条规则进行了多组真实的 HA-IoT 案例研究。实证结果表明，门神仅需10秒即可发现违规行为并生成规则修复建议。
Recent advances and industry standards in Internet of Things (IoT) have accelerated the real-world adoption of connected devices. To manage this hybrid system of digital real-time devices and analog environments, the industry has pushed several popular home automation IoT (HA-IoT) frameworks, such as If-This-Then-That (IFTTT), Apple HomeKit, and Google Brillo. Typically, users author device interactions by specifying the triggering sensor event and the triggered device command. In this seemingly simple software system, two dominant factors govern the system confidence properties with respect to the physical world. First, IoT users are largely nonexperts who lack the comprehensive consideration regarding potential impact and joint effect with existing rules. Second, while the increasing complexity of IoT devices enables fine-grained control (e.g., heater temperature) of continuous real-time environments, even two simply connected devices can have a huge state space to explore. In fact, bugs that wrongfully control devices and home appliances can have ramifications on system correctness and even user physical safety. It is crucial to help users to make sure the system they created meets their expectation. In this article we introduce how techniques from hybrid automata can be practically applied to assist nonexpert IoT users in the confidence checking of such hybrid HA-IoT systems. We propose an automated framework for end-to-end programming assistance. We build and check the Linear Hybrid Automata (LHA) model of the system automatically. We also present a quantifier elimination-based method to analyze the counterexample found and synthesize fix suggestions. We implemented a platform, MenShen, based on this framework and proposed techniques. We conducted sets of real HA-IoT case studies with up to 46 devices and 65 rules. Empirical results show that MenShen can find violations and generate rule fix suggestions in only 10 seconds.
登录
查看更多内容
DOI：
10.1007/978-3-319-25141-7_2
发表时间：
2015-10
期刊：
--
影响因子：
--
作者：
Stefan Schupp;E. Ábrahám;Xin Chen;Ibtissem Ben Makhlouf;Goran Frehse;S. Sankaranarayanan;S. Kowalewski
通讯作者：
Stefan Schupp;E. Ábrahám;Xin Chen;Ibtissem Ben Makhlouf;Goran Frehse;S. Sankaranarayanan;S. Kowalewski
DOI：
10.1007/bfb0027241
发表时间：
1995
期刊：
--
影响因子：
--
作者：
T. Henzinger;H. Wong-Toi
通讯作者：
T. Henzinger;H. Wong-Toi
DOI：
10.1016/b978-044450813-3/50026-6
发表时间：
2001
期刊：
--
影响因子：
--
作者：
E. Clarke;Holger Schlingloff
通讯作者：
E. Clarke;Holger Schlingloff
DOI：
10.1007/978-3-642-61455-2_16
发表时间：
1996-09
期刊：
--
影响因子：
--
作者：
Edmund M. Clarke;O. Grumberg;D. E. Long
通讯作者：
Edmund M. Clarke;O. Grumberg;D. E. Long
DOI：
10.1016/s0065-2458(03)58003-2
发表时间：
2003
期刊：
Adv. Comput.
影响因子：
--
作者：
Armin Biere
通讯作者：
Armin Biere