浏览全部资源
扫码关注微信
面向事件驱动智能家居物联网系统的自动化配置、仿真与验证平台
Automated configuration,simulation and verification platform for event-driven home automation IoT system
- 物联网学报 2019年3卷第3期 页码：90-101
- 作者机构：
- 作者简介：
[ "张秋萍（1994- ），女，江苏苏州人，南京大学硕士生，主要研究方向为形式化方法和模型检验。" ]
[ "王熙灶（1995- ），男，江西高安人，南京大学博士生，主要研究方向为程序分析和程序验证。" ]
[ "沈思远（1997- ），男，湖北黄冈人，南京大学硕士生，主要研究方向为以太坊智能合约代码优化、测试和验证。" ]
[ "张时雨（1995- ），女，辽宁阜新人，南京大学硕士生，主要研究方向为形式化方法和模型检验。" ]
[ "卜磊（1983- ），男，江苏东台人，博士，南京大学副教授、博士生导师，主要研究方向为形式化方法、模型检验、实时混成系统和信息物理融合系统。" ]
[ "李宣东（1963- ），男，湖南邵东人，博士，南京大学教授、博士生导师，主要研究方向为软件工程、软件建模与分析、软件测试与验证。" ]
- 基金信息：国家重点研发计划基金资助项目;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)
DOI：10.11959/j.issn.2096-3750.2019.00124
中图分类号： TP311纸质出版日期：2019-09-30，
网络出版日期：2019-09，
- 稿件说明：
移动端阅览
张秋萍, 王熙灶, 沈思远, 等. 面向事件驱动智能家居物联网系统的自动化配置、仿真与验证平台[J]. 物联网学报, 2019,3(3):90-101.
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.
张秋萍, 王熙灶, 沈思远, 等. 面向事件驱动智能家居物联网系统的自动化配置、仿真与验证平台[J]. 物联网学报, 2019,3(3):90-101. DOI： 10.11959/j.issn.2096-3750.2019.00124.
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.
0
浏览量
1205
下载量
0
CSCD
- 网络PDF下载
- Meta-XML下载
- BibTeX下载
- Endnote下载
- RefMan 下载
- NoteExpress下载
- NoteFirst下载
关联资源
相关文章
相关作者
相关机构
- 技术支持由北京北大方正电子有限公司提供 京ICP备09064830号-19
京公网安备11010802024621 - 本系统建议在Chrome、 IE9+ 以上版本浏览器阅读本站内容，360浏览器请切换至极速模式
- Cookies帮助我们提供服务并提供个性化体验。使用本网站，即表示您同意我们使用Cookies
- 总访问量：42480 今日访问量：275