TY - GEN
T1 - A Verification Method for Security and Safety of IoT Applications through DSM Language and Lustre
AU - Tang, Wentao
AU - Feng, Hao
AU - Hisazumi, Kenji
AU - Fukuda, Akira
N1 - Publisher Copyright:
© 2020 ACM.
PY - 2020/3/19
Y1 - 2020/3/19
N2 - 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.
AB - 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.
KW - Code Generating
KW - IoT; DSML
KW - Lustre
KW - Model-Checking
KW - Smart House
UR - http://www.scopus.com/inward/record.url?scp=85092149415&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85092149415&partnerID=8YFLogxK
U2 - 10.1145/3388176.3388211
DO - 10.1145/3388176.3388211
M3 - Conference contribution
AN - SCOPUS:85092149415
T3 - ACM International Conference Proceeding Series
SP - 166
EP - 170
BT - Proceedings of the 2020 3rd International Conference on Information Science and System, ICISS 2020
PB - Association for Computing Machinery
T2 - 3rd International Conference on Information Science and System, ICISS 2020
Y2 - 19 March 2020 through 22 March 2020
ER -