Automated configuration,simulation and verification platform for event-driven home automation IoT system

Qiuping ZHANG; Xizao WANG; Siyuan SHEN; Shiyu ZHANG; Lei BU; Xuandong LI

doi:10.11959/j.issn.2096-3750.2019.00124

您当前的位置：

首页 >

文章列表页 >

Automated configuration,simulation and verification platform for event-driven home automation IoT system

Service and Application | 更新时间：2024-06-05

- Automated configuration,simulation and verification platform for event-driven home automation IoT system
- Chinese Journal on Internet of Things Vol. 3, Issue 3, Pages: 90-101(2019)
- 作者机构：
- 作者简介：
- 基金信息：
- DOI：10.11959/j.issn.2096-3750.2019.00124
  CLC： TP311
- Published：30 September 2019，
  
  Published Online：2019-09，
- 稿件说明：
移动端阅览
QIUPING ZHANG, XIZAO WANG, SIYUAN SHEN, et al. Automated configuration,simulation and verification platform for event-driven home automation IoT system. [J]. Chinese journal on internet of things, 2019, 3(3): 90-101.
DOI：

QIUPING ZHANG, XIZAO WANG, SIYUAN SHEN, et al. Automated configuration,simulation and verification platform for event-driven home automation IoT system. [J]. Chinese journal on internet of things, 2019, 3(3): 90-101. DOI： 10.11959/j.issn.2096-3750.2019.00124.

摘要

以IFTTT为代表的事件驱动型物联网系统编程框架为用户构建满足其需求的智能家居物联网系统提供了极大的便利，但也带来了严峻的安全隐患。针对此问题，设计并实现了“门神”，这是一个基于模型检验的事件驱动型物联网系统配置、仿真与验证平台。用户可以在门神中自定义其系统，并进行一键式模型驱动的仿真及验证、自动检测并重现错误场景，从而理解系统行为并提升其安全性。通过大量实验可知，门神能在86.7%的案例中发现安全隐患，且平均耗时仅为0.7 s。

Abstract

The IFTTT style event-driven programming paradigm benefits normal users to build their own customized home automation Internet of things (IoT) system

meanwhile

it also brings serious safety and security risks.To handle this problem

Menshen was designed and implemented

an automated configuration

simulation and verification platform for event-driven home automation IoT system based on model checking.Users can easily set up their own smart home systems in Menshen

and conduct simulation and verification in a push-button style.Menshen could further demonstrate the error trace to help users to understand the behavior of the system and increase the safety and security of the system.An experiment with a large number of cases is carried out

and the results show that 86.7% cases are error-prone

and the verification only took 0.7 seconds in average.

关键词

物联网IFTTT框架系统安全模型检验

Keywords

Internet of thingsIFTTT frameworksystem securitymodel checking

references

UR B, MCMANUS E, HO M P Y ,et al. Practical trigger-action programming in the smart home[C]// Sigchi Conference on Human Factors in Computing Systems. ACM, 2014: 803-812.

LEELAPRUTE P, NAKAMURA M, TSUCHIYA T ,et al. Describing and verifying integrated services of home network systems[C]// Asia-Pacific Software Engineering Conference. IEEE, 2005: 549-558.

CORNO F, SANAULLAH M . Modeling and formal verification of smart environments[J]. Security ＆ Communication Networks, 2015,7(10): 1582-1598.

LIANG C J M, LANE N D, ZHAO F ,et al. SIFT:building an Internet of safe things[C]// International Conference on Information Processing in Sensor Networks. ACM, 2015: 298-309.

LIANG C J M, BU L, LI Z ,et al. Systematically debugging IoT control system correctness for building automation[C]// ACM International Conference on Systems for Energy-Efficient Built Environments. ACM, 2016: 133-142.

BU L, XIONG W, LIANG C J M ,et al. Systematically ensuring the confidence of real-time home automation IoT systems[J]. ACM Transactions on Cyber-Physical Systems, 2018,2(3): 1-23.

BAIER C, KATOEN J P . Principles of model checking[M]. Cambridge: The MIT PressPress, 2008.

HOLZMANN G J . The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997,23(5): 279-295.

CIMATTI A, CLARKE E, GIUNCHIGLIA F ,et al. NuSMV:a new symbolic model checker[J]. International Journal on Software Tools for Technology Transfer, 2000,2(4): 410-425.

BU L, LI Y, WANG L ,et al. BACH :bounded reachability checker for linear hybrid automata[C]// Formal Methods in Computer-Aided Design. IEEE, 2008: 1-4.

CROCKFORD D . The application/JSON media type for JavaScript object notation (JSON)[J]. RFC, 2006,13(4): 250-251.

CLARKE E M, EMERSON E A . Design and synthesis of synchronization skeletons using branching time temporal logic[C]// The Workshop on Logic of Programs. Springer, 1981: 52-71.

PNUELI A . The temporal logic of programs[M]. Rehovot: Weizmann Science PressPress, 1977.

MUNIR S, STANKOVIC J A . Depsys:dependency aware integration of cyber-physical systems for smart homes[C]// ACM/IEEE International Conference on Cyber-Physical Systems. IEEE, 2014: 127-138.

SURBATOVICH M, ALJURAIDAN J, BAUER L ,et al. Some recipes can do more than spoil your appetite:analyzing the security and privacy risks of IFTTT recipes[C]// International World Wide Web Conference. ACM, 2017: 1501-1510.

LI H, ZHOU X . Study on security architecture for Internet of things[C]// International Conference on Applied Informatics and Communication. Springer, 2011: 404-411.

RIAHI A, CHALLAL Y, NATALIZIO E ,et al. A systemic approach for IoT security[C]// IEEE International Conference on Distributed Computing in Sensor Systems. IEEE, 2013: 351-355.

RIERA B,VIGÁRIO B . HOME I/O and FACTORY I/O:a virtual house and a virtual plant for control education[J]. IFAC-Papers on Line, 2017,50(1): 9144-9149.

ALSHAMMARI N, ALSHAMMARI T, SEDKY M ,et al. OpenSHS:open smart home simulator[J]. Sensors, 2017,17(5):1003.

Views

1205

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Reinforcement learning-based channel access mechanism for multi-base station slotted Aloha with cooperative reception

A survey of federated learning for 6G networks

New flexible sensor for the internet of things

Optical wireless communication and internet of things

Study of international standard ISO/IEC 30144: 2020 applied in intelligent substation auxiliary monitoring

Related Author

HUANG Yuankang

ZHAN Wen

SUN Xinghua

Guanglei GENG

Bo GAO

Ke XIONG

Pingyi FAN

Yang LU

Related Institution

Sun Yat-sen University

Sun Yat-sen University Shenzhen Campus

School of Computer and Information Technology, Beijing Jiaotong University

Engineering Research Center of Network Management Technology for High Speed Railway of Ministry of Education, Beijing Jiaotong University

National Research Center for Information Science and Technology, Tsinghua University

⁰