Project/Area Number |
23H03370
|
Research Category |
Grant-in-Aid for Scientific Research (B)
|
Allocation Type | Single-year Grants |
Section | 一般 |
Review Section |
Basic Section 60050:Software-related
|
Research Institution | Osaka University |
Principal Investigator |
土屋 達弘 大阪大学, 大学院情報科学研究科, 教授 (30283740)
|
Co-Investigator(Kenkyū-buntansha) |
林原 尚浩 京都産業大学, 情報理工学部, 准教授 (20397227)
緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
中川 博之 大阪大学, 大学院情報科学研究科, 准教授 (40508834)
|
Project Period (FY) |
2023-04-01 – 2027-03-31
|
Project Status |
Granted (Fiscal Year 2023)
|
Budget Amount *help |
¥18,330,000 (Direct Cost: ¥14,100,000、Indirect Cost: ¥4,230,000)
Fiscal Year 2023: ¥5,850,000 (Direct Cost: ¥4,500,000、Indirect Cost: ¥1,350,000)
|
Keywords | ディペンダブルシステム / 分散システム / モデルチェッキング / 機密実行 |
Outline of Research at the Start |
複数のサーバを協調させることでサービスを実現する分散システムは,現代の情報化社会において欠かせない.このような分散システムを,誤りや悪意ある攻撃に耐えられるように,信頼性高く,つまり,ディペンダブルに実現するためには,その設計の正しさを検証することが重要である.本研究では,分散システムを機械的に検証するために,モデルチェッキングと呼ばれる手法を発展させる.具体的には,現状,サーバの台数が小さい場合にしか適用できないこの手法を,より規模の大きいシステムにも適用できるようにする.さらに,最近のCPUがもつ機密実行機能を利用した分散システムの検証も可能にする.
|