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

doi:10.11959/j.issn.2096-3750.2019.00124

物联网学报 ›› 2019, Vol. 3 ›› Issue (3): 90-101.doi: 10.11959/j.issn.2096-3750.2019.00124

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

张秋萍,王熙灶,沈思远,张时雨,卜磊(),李宣东

南京大学软件新技术国家重点实验室，江苏南京 210023

修回日期:2019-04-06 出版日期:2019-09-30 发布日期:2019-10-14
作者简介:张秋萍（1994- ），女，江苏苏州人，南京大学硕士生，主要研究方向为形式化方法和模型检验。|王熙灶（1995- ），男，江西高安人，南京大学博士生，主要研究方向为程序分析和程序验证。|沈思远（1997- ），男，湖北黄冈人，南京大学硕士生，主要研究方向为以太坊智能合约代码优化、测试和验证。|张时雨（1995- ），女，辽宁阜新人，南京大学硕士生，主要研究方向为形式化方法和模型检验。|卜磊（1983- ），男，江苏东台人，博士，南京大学副教授、博士生导师，主要研究方向为形式化方法、模型检验、实时混成系统和信息物理融合系统。|李宣东（1963- ），男，湖南邵东人，博士，南京大学教授、博士生导师，主要研究方向为软件工程、软件建模与分析、软件测试与验证。
基金资助:
国家重点研发计划基金资助项目(2017YFA0700604);国家自然科学基金资助项目(61632015);国家自然科学基金资助项目(61572249);国家自然科学基金资助项目(61561146394)

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

State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210023,China

Revised:2019-04-06 Online:2019-09-30 Published:2019-10-14
Supported by:
The National Key R＆D Program of China(2017YFA0700604);The National Natural Science Foundation of China(61632015);The National Natural Science Foundation of China(61572249);The National Natural Science Foundation of China(61561146394)

摘要/Abstract

摘要：

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

关键词: 物联网, IFTTT框架, 系统安全, 模型检验

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

中图分类号:

TP311

张秋萍,王熙灶,沈思远,张时雨,卜磊,李宣东. 面向事件驱动智能家居物联网系统的自动化配置、仿真与验证平台[J]. 物联网学报, 2019, 3(3): 90-101.

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.

图/表 11

图1

图2

图3

图4

图5

图6

图7

图8

图9

表1

图10

参考文献 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.

	案例数量	需验证案例数量	验证未通过案例数量	平均包含规约数量	平均未通过规约数量	平均验证时间/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

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 11

参考文献 19

相关文章 15

Metrics

推荐阅读 0

[1]	吴靖, 李晟, 张景, 辛明, 陶若文, 周舟, 潘力佳, 施毅. 面向物联网的新型柔性传感器[J]. 物联网学报, 2023, 7(2): 1-14.
[2]	梁峻阁, 宋怡然, 孙杨帆, 计樱莹, 潘力佳, 施毅. 基于可穿戴与可植入技术的人体健康物联网研究进展[J]. 物联网学报, 2023, 7(2): 26-34.
[3]	耿光磊, 高博, 熊轲, 樊平毅, 陆杨, 王煜炜. 联邦学习赋能6G网络综述[J]. 物联网学报, 2023, 7(2): 50-66.
[4]	卫浓钰, 江子龙, 陈芳炯. 基于位置信息和能量均衡的声电协同网络AODV[J]. 物联网学报, 2023, 7(1): 27-36.
[5]	申滨, 李银波, 梁枭伟. 基于增强加权质心定位的认知物联网用户频谱接入控制[J]. 物联网学报, 2023, 7(1): 93-108.
[6]	汪静, 何乐生, 李忠红, 李路迟, 杨航. 物联网轻量级认证加密算法ASCON的软硬件协同设计[J]. 物联网学报, 2022, 6(4): 139-148.
[7]	蒋伟进, 罗田甜, 杨莹, 李恩, 周文颖. 物联网环境下基于区块链技术的私有数据访问控制模型[J]. 物联网学报, 2022, 6(4): 169-182.
[8]	邢方圆, 贺诗波, 孙铭阳, 陈积明. 基于“云-管-边-端”物联网架构的碳排放监测[J]. 物联网学报, 2022, 6(4): 53-64.
[9]	张在琛, 尤肖虎, 党建, 吴亮, 朱秉诚, 陈绩, 汪磊. 无线光通信与物联网[J]. 物联网学报, 2022, 6(3): 1-13.
[10]	黄诺, 刘伟杰, 龚晨. 面向工业物联网的拍赫兹通信[J]. 物联网学报, 2022, 6(3): 37-46.
[11]	孙君, 赵尚维康. 工业物联网中基于Sarsa算法的节能计算卸载方案[J]. 物联网学报, 2022, 6(3): 82-90.
[12]	刘杨, 李崔灿, 彭木根. 低功耗水下物联网：愿景与关键技术[J]. 物联网学报, 2022, 6(2): 1-9.
[13]	杨靖, 谢金凤, 陈怡. 我国智慧城市场景中物联网终端评测与认证体系研究[J]. 物联网学报, 2022, 6(2): 26-37.
[14]	罗丹, 徐茹枝, 关志涛. 物联网环境中基于深度学习的差分隐私预算优化方法[J]. 物联网学报, 2022, 6(2): 65-76.
[15]	罗梓珲, 江呈羚, 刘亮, 郑霄龙, 马华东. 基于深度强化学习的智能车间调度方法研究[J]. 物联网学报, 2022, 6(1): 53-64.