Enhancement of Formal Verification for IoT Systems

2023 Fiscal Year Final Research Report

• Project/Area Number: 19H04084
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Kyoto University
• Principal Investigator: Suenaga Kohei 京都大学, 情報学研究科, 准教授 (70633692)
• Co-Investigator(Kenkyū-buntansha): 五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456) ; 海野 広志 筑波大学, システム情報系, 准教授 (80569575) ; 池渕 未来 京都大学, 情報学研究科, 助教 (70961796)
• Project Period (FY): 2019-04-01 – 2024-03-31
• Keywords: ハイブリッドシステム / モデル検査 / プログラム検証 / 形式検証 / ブラックボックス検査 / モニタリング / PDR

Outline of Final Research Achievements

This research project mainly focused on formal verification methods for hybrid systems, which are mathematical models of IoT systems. The main research results include (1) extension of the PDR model checking algorithm for verifying hybrid systems, and (2) elucidation of the essence of PDR using lattice theory. In addition, the following results were obtained: type-based verification for imperative languages equipped with pointers, methods for efficiently testing systems with black boxes, and methods for oblivious monitoring that allow monitoring of data containing sensitive information while it remains encrypted.

Free Research Field

形式検証

Academic Significance and Societal Importance of the Research Achievements

この研究課題では，IoTシステムの安全性を確保するための新しい形式検証手法について扱った．特に，ソフトウェアと物理的プロセスが融合したハイブリッドシステムの安全性を保証するために，PDR (Property-Directed Reachability) と呼ばれるモデル検査手法を拡張した．この技術により，IoTデバイスが互いに安全に連携し，データを交換できるようになる．この成果は，社会全体のIoT技術の信頼性と効率を向上させ，高度なデジタル化社会の発展に大きく貢献する成果である．