研究課題/領域番号 |
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千円)
|
キーワード | プログラム検証 / 形式検証 / IoT / モデル検査 / PDR / 強化学習 / 機械学習 / ハイブリッドシステム / 形式手法 |
研究開始時の研究の概要 |
IoT システムの安全性保証は,IoT の普及とその safety-critical な場面での利用が進むにつれ,大きな社会的課題となりつつある.この課題の解決のために大規模な IoT システムの非自明な安全性を保証するための形式検証手法を提案する.具体的には,ソフトウェア検証の分野で成功を収めている検証手法を拡張し,人間が援助することによって自動検証プロセスをガイドするための手法を目指す.
|
研究実績の概要 |
本研究課題での主要なトピックの一つである仕様手動到達性 (Property Directed Reachability; PDR) を用いたモデル検査手法について,理論面で大きな成果があった.PDRは,従来、実装の詳細を伴う手続き型言語での定義が主流であり,その本質的な計算プロセスが理解しにくい状況であった.そこで我々は,束論 (Lattice Theory) を用いてPDRを理論的に再定義することで,その本質を明らかにする新しい定義を提案した.この新たな定義により,確率的システムをはじめとする様々なシステムに対する PDR が統一的に理解できることを示した.さらに,この定義に基づいた検証器を実装した.この実装は,様々なシステムの性質を差分的に実装することで,そのシステムのためのPDRを自動的に導出できるような一般的な実装となっており,その汎用性が従来実装に比して非常に高くなっている.本研究の成果を,2022年の国際会議 Computer Aided Verification (CAV) において発表した.
|
現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
上記の CAV での発表を始め,関連する成果が多く上がっており,進捗は順調である.
|
今後の研究の推進方策 |
前年度までの強化学習を用いたモデル検査器の高速化手法や,PDR の再定義等の手法をさらに進化させ,IoT において多く現れるハイブリッドシステムの検証手法として結実させる方向に研究をすすめる予定である.
|