| 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 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
池渕 未来 京都大学, 情報学研究科, 助教 (70961796)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Project Status |
Granted (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 | プログラム検証 / 形式検証 / IoT / モデル検査 / PDR / 強化学習 / 機械学習 / ハイブリッドシステム / 形式手法 |
|---|
| Outline of Research at the Start |
IoT システムの安全性保証は，IoT の普及とその safety-critical な場面での利用が進むにつれ，大きな社会的課題となりつつある．この課題の解決のために大規模な IoT システムの非自明な安全性を保証するための形式検証手法を提案する．具体的には，ソフトウェア検証の分野で成功を収めている検証手法を拡張し，人間が援助することによって自動検証プロセスをガイドするための手法を目指す．
|
| Outline of Annual Research Achievements |
本研究課題での主要なトピックの一つである仕様手動到達性 (Property Directed Reachability; PDR) を用いたモデル検査手法について，理論面で大きな成果があった．PDRは，従来、実装の詳細を伴う手続き型言語での定義が主流であり，その本質的な計算プロセスが理解しにくい状況であった．そこで我々は，束論 (Lattice Theory) を用いてPDRを理論的に再定義することで，その本質を明らかにする新しい定義を提案した．この新たな定義により，確率的システムをはじめとする様々なシステムに対する PDR が統一的に理解できることを示した．さらに，この定義に基づいた検証器を実装した．この実装は，様々なシステムの性質を差分的に実装することで，そのシステムのためのPDRを自動的に導出できるような一般的な実装となっており，その汎用性が従来実装に比して非常に高くなっている．本研究の成果を，2022年の国際会議 Computer Aided Verification (CAV) において発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
上記の CAV での発表を始め，関連する成果が多く上がっており，進捗は順調である．
|
| Strategy for Future Research Activity |
前年度までの強化学習を用いたモデル検査器の高速化手法や，PDR の再定義等の手法をさらに進化させ，IoT において多く現れるハイブリッドシステムの検証手法として結実させる方向に研究をすすめる予定である．
|
Report
(3 results)
Research Products
(24 results)
