| 研究課題/領域番号 |
19H04084
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| 研究分担者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
池渕 未来 京都大学, 情報学研究科, 助教 (70961796)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
17,030千円 (直接経費: 13,100千円、間接経費: 3,930千円)
2023年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2022年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2021年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2020年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2019年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
|
|---|
| キーワード | ハイブリッドシステム / モデル検査 / プログラム検証 / 形式検証 / ブラックボックス検査 / モニタリング / PDR / IoT / 強化学習 / 機械学習 / 形式手法 |
|---|
| 研究開始時の研究の概要 |
IoT システムの安全性保証は，IoT の普及とその safety-critical な場面での利用が進むにつれ，大きな社会的課題となりつつある．この課題の解決のために大規模な IoT システムの非自明な安全性を保証するための形式検証手法を提案する．具体的には，ソフトウェア検証の分野で成功を収めている検証手法を拡張し，人間が援助することによって自動検証プロセスをガイドするための手法を目指す．
|
| 研究成果の概要 |
IoT システムの数学的なモデルであるハイブリッドシステムのための形式検証手法を主眼において研究した．主な研究成果としては (1) ハイブリッドシステム検証のための PDR モデル検査アルゴリズムの拡張，(2) 束論を用いた PDR の本質の解明が得られた．この他にも，IoT システムに関わるソフトウェアの主要な実装言語であるポインタを含む命令型言語のための型理論に基づく検証手法や，ブラックボックスを含むシステムを効率的にテストする手法，機微情報を含むデータを暗号文のままでモニタリング可能とする秘匿モニタリング手法等の成果が得られた．
|
| 研究成果の学術的意義や社会的意義 |
この研究課題では，IoTシステムの安全性を確保するための新しい形式検証手法について扱った．特に，ソフトウェアと物理的プロセスが融合したハイブリッドシステムの安全性を保証するために，PDR (Property-Directed Reachability) と呼ばれるモデル検査手法を拡張した．この技術により，IoTデバイスが互いに安全に連携し，データを交換できるようになる．この成果は，社会全体のIoT技術の信頼性と効率を向上させ，高度なデジタル化社会の発展に大きく貢献する成果である．
|
