| 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
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥17,030,000 (Direct Cost: ¥13,100,000、Indirect Cost: ¥3,930,000)
Fiscal Year 2023: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2022: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2021: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2020: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2019: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
|
|---|
| Keywords | ハイブリッドシステム / モデル検査 / プログラム検証 / 形式検証 / ブラックボックス検査 / モニタリング / PDR / IoT / 強化学習 / 機械学習 / 形式手法 |
|---|
| Outline of Research at the Start |
IoT システムの安全性保証は，IoT の普及とその safety-critical な場面での利用が進むにつれ，大きな社会的課題となりつつある．この課題の解決のために大規模な IoT システムの非自明な安全性を保証するための形式検証手法を提案する．具体的には，ソフトウェア検証の分野で成功を収めている検証手法を拡張し，人間が援助することによって自動検証プロセスをガイドするための手法を目指す．
|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
この研究課題では，IoTシステムの安全性を確保するための新しい形式検証手法について扱った．特に，ソフトウェアと物理的プロセスが融合したハイブリッドシステムの安全性を保証するために，PDR (Property-Directed Reachability) と呼ばれるモデル検査手法を拡張した．この技術により，IoTデバイスが互いに安全に連携し，データを交換できるようになる．この成果は，社会全体のIoT技術の信頼性と効率を向上させ，高度なデジタル化社会の発展に大きく貢献する成果である．
|
