面向事件驱动智能家居物联网系统的自动化配置、仿真与验证平台

doi:10.11959/j.issn.2096-3750.2019.00124

Abstract

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.

Key words: Internet of things, IFTTT framework, system security, model checking

CLC Number:

TP311

Qiuping ZHANG,Xizao WANG,Siyuan SHEN,Shiyu ZHANG,Lei BU,Xuandong LI. 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.

Figures/Tables 11

References 19

[1]	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.
[2]	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.
[3]	CORNO F , SANAULLAH M . Modeling and formal verification of smart environments[J]. Security ＆ Communication Networks, 2015,7(10): 1582-1598.
[4]	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.
[5]	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.
[6]	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.
[7]	BAIER C , KATOEN J P . Principles of model checking[M]. Cambridge: The MIT PressPress, 2008.
[8]	HOLZMANN G J . The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997,23(5): 279-295.
[9]	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.
[10]	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.
[11]	CROCKFORD D . The application/JSON media type for JavaScript object notation (JSON)[J]. RFC, 2006,13(4): 250-251.
[12]	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.
[13]	PNUELI A . The temporal logic of programs[M]. Rehovot: Weizmann Science PressPress, 1977.
[14]	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.
[15]	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.
[16]	LI H , ZHOU X . Study on security architecture for Internet of things[C]// International Conference on Applied Informatics and Communication. Springer, 2011: 404-411.
[17]	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.
[18]	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.
[19]	ALSHAMMARI N , ALSHAMMARI T , SEDKY M ,et al. OpenSHS:open smart home simulator[J]. Sensors, 2017,17(5):1003.

Metrics

Recommended 0

No Suggested Reading articles found!

	案例数量	需验证案例数量	验证未通过案例数量	平均包含规约数量	平均未通过规约数量	平均验证时间/s
单用户	91	88	74	2.70	1.60	0.55
多用户	59	59	56	5.08	2.83	0.94
总体	150	147	130	3.64	2.09	0.7

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

RichHTML

PDF下载

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 11

References 19

Related Articles 15

Metrics

Recommended 0

[1]	Jing WU, Sheng LI, Jing ZHANG, Ming XIN, Ruowen TAO, Zhou ZHOU, Lijia PAN, Yi SHI. New flexible sensor for the internet of things [J]. Chinese Journal on Internet of Things, 2023, 7(2): 1-14.
[2]	Guanglei GENG, Bo GAO, Ke XIONG, Pingyi FAN, Yang LU, Yuwei WANG. A survey of federated learning for 6G networks [J]. Chinese Journal on Internet of Things, 2023, 7(2): 50-66.
[3]	Bin SHEN, Yinbo LI, Xiaowei LIANG. Spectrum access control for cognitive internet of things users based on enhanced weighted centroid localization [J]. Chinese Journal on Internet of Things, 2023, 7(1): 93-108.
[4]	Jun SUN, Shangweikang ZHAO. Energy-saving computation offloading scheme based on Sarsa algorithm in industrial internet of things [J]. Chinese Journal on Internet of Things, 2022, 6(3): 82-90.
[5]	Zaichen ZHANG, Xiaohu YOU, Jian DANG, Liang WU, Bingcheng ZHU, Ji CHEN, Lei WANG. Optical wireless communication and internet of things [J]. Chinese Journal on Internet of Things, 2022, 6(3): 1-13.
[6]	Nuo HUANG, Weijie LIU, Chen GONG. Industrial IoT oriented petahertz communication [J]. Chinese Journal on Internet of Things, 2022, 6(3): 37-46.
[7]	Wei WANG, Renqian GU, Li3 PENG, Jijun ZHAO, Zhongcheng WEI, Cunxi CHANG. Robust optimization of air based relay for internet of things based on UAV [J]. Chinese Journal on Internet of Things, 2022, 6(1): 101-112.
[8]	Mingjuan WU, Shuyi CHEN, Haitao LIU. Study of international standard ISO/IEC 30144: 2020 applied in intelligent substation auxiliary monitoring [J]. Chinese Journal on Internet of Things, 2022, 6(1): 123-132.
[9]	Hao JIANG, Hongming CHEN, Yilong CAO, Haoyang CUI. Comparison of MIMO based on high capacity LPWAN technology TurMass^TM and LoRa [J]. Chinese Journal on Internet of Things, 2021, 5(4): 54-61.
[10]	Zhongcheng WEI, Xinqiu ZHANG, Bin LIAN, Wei WANG, Jijun ZHAO. A survey on Wi-Fi signal based identification technology [J]. Chinese Journal on Internet of Things, 2021, 5(4): 107-119.
[11]	Yinghai XIE, Yu ZHANG. Electricity meter area identification technology based on channel coding theory [J]. Chinese Journal on Internet of Things, 2021, 5(4): 137-144.
[12]	Yiyang HU, Lina QI. Channel estimation method of massive MIMO-OFDM system based on adaptive compressed sensing [J]. Chinese Journal on Internet of Things, 2021, 5(3): 78-85.
[13]	Wei WANG, Yajing LIANG, Li PENG, Zhongcheng WEI, Jijun ZHAO. Node clustered deployment of emergency Internet of things based on UAV with equipment access restriction [J]. Chinese Journal on Internet of Things, 2021, 5(3): 97-105.
[14]	Ling TAN, Shanshan RONG, Jingming XIA, Sarker SAJIB, Wenjie MA. Real-time diagnosis of multi-category skin diseases based on IR-VGG [J]. Chinese Journal on Internet of Things, 2021, 5(3): 115-125.
[15]	Siqi SUN. Analysis and prospects of the development of the industrial Internet in the petrochemical industry [J]. Chinese Journal on Internet of Things, 2021, 5(3): 126-132.