A Verification Method for Security and Safety of IoT Applications Through DSM Language and Lustre.

Development of Internet of Things (IoT) brings a variety of IoT applications that involve housing, navigation, payment, and healthcare. Since IoT applications play an important role in our lives, security is critical to these applications and must be guaranteed. In order to realize this, the paper proposes a pre-execution verification method for downloaded IoT applications, which meets security and safety requirements of users using model checking. The model checking requires special models for verification, which is difficult to describe for developers. So we introduce a domain-specific modeling language (DSML) to describe IoT application and a generator from the DSML into the model to pre-execution verification and execution. Also, as a case study, we provide a study of our method used in a smart house application, which is one of the most representative examples in IoT applications.