物联网学报 (Sep 2019)
Automated configuration,simulation and verification platform for event-driven home automation IoT system
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.