Testing and model checking of IoT protocols

2020 Fiscal Year Final Research Report

• Project/Area Number: 17H01719
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: The University of Tokyo
• Principal Investigator: Hagiya Masami 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
• Co-Investigator(Kenkyū-buntansha): 田辺 良則 鶴見大学, 文学部, 教授 (60443199)
• Project Period (FY): 2017-04-01 – 2020-03-31
• Keywords: 仕様記述 / ソフトウェア検証 / ソフトウェアテスト / モデルベーステスト / IoT / MQTT

Outline of Final Research Achievements

We have developed a model-based test method to enable verification of controller software in an IoT environment. By representing the same type of device with one state transition system (model) and introducing a mechanism that manages the number of virtual instances existing in each state (state distribution), we can test a system consisting of a large number of devices with a very low load. In addition, we can significantly reduce the test time by running the entire test tool under a scheduler that runs in virtual time and skipping virtual time when possible. In addition, MQTT transmission / reception can be described in the model, and network disconnection / delay can be simulated by the tool.

Free Research Field

ソフトウェア科学・ソフトウェア工学

Academic Significance and Societal Importance of the Research Achievements

センサなどのデバイスから家電・自動車までがネットワークにつながるIoT（モノのインターネット）において、システムが正しく安全に動作することを検証する手法を開発した。温度計や電力計などの多数のデバイスが長時間に亘って動作するシステムを対象とする。そのようなシステムを制御するソフトウェア（コントローラ）を検証するために、コントローラが動作する環境を効率よくシミュレートする手法を研究し、実際にテストツールを実装した。そのために、個々のデバイスではなくデバイスの分布をシミュレートする方法、仮想時間によりシミュレーションの時間を短縮する方法、システム内の通信をシミュレートする方法等を開発した。