2023 Fiscal Year Annual Research Report
| Project/Area Number |
19H04084
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
池渕 未来 京都大学, 情報学研究科, 助教 (70961796)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Keywords | モデル検査 / PDR / IoT |
|---|
| Outline of Annual Research Achievements |
IoTシステムのための形式検証手法として，以下の手法について研究を行った．
確率的な挙動を行い，かつ内部動作がブラックボックスであるようなIoTシステムを，モデル検査と動的検査を組み合わせて検証する手法を研究した．この手法では，ブラックボックスシステムに対してシステマティックに生成された入力を与え，その挙動に関するデータを得ることで，この挙動を模倣するMDPを得る．その上で，得られたMDPに対して確率的モデル検査を適用し，仕様の充足可能性を最大化するようなスケジューラを得る．このスケジューラをブラックボックスシステムに対して適用し，実際に動作させたうえで，同じ確率で仕様が充足されるかどうかを判断する．もし異なる確率が得られた場合には，再度MDPの学習を進め，より正確なMDPを得ることで，ブラックボックスシステムの検査を継続する．この手法により，確率的挙動を示すブラックボックスシステムの仕様の充足確率を，従来手法より高速かつ正確に見積もれることを実験的に確認した．
また，IoTシステムの重要な構成要素であるハイブリッドシステムについて，ブラックボックスなハイブリッドシステムからその挙動を模倣するハイブリッドオートマトンを得る手法を提案した．この手法では，ハイブリッドシステムに対して様々な入力を与え，得られた出力からハイブリッドオートマトンを構成する．上記の手法と同様に，ブラックボックス検査への応用が期待される．
|
| Research Progress Status |
令和5年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和5年度が最終年度であるため、記入しない。
|
Research Products
(5 results)
-
-
[Journal Article] Goal-Aware RSS for Complex Scenarios via Program Logic2023
Author(s)
Hasuo Ichiro、Eberhart Clovis、Haydon James、Dubut J?r?my、Bohrer Rose、Kobayashi Tsutomu、Pruekprasert Sasinee、Zhang Xiao-Yi、Pallas Erik Andr?、Yamada Akihisa、Suenaga Kohei、Ishikawa Fuyuki、Kamijo Kenji、Shinya Yoshiyuki、Suetomi Takamasa
-
Journal Title
IEEE Transactions on Intelligent Vehicles
Volume: 8
Pages: 3040～3072
DOI
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
