物理情報システムに対する軽量検証の、オートマトン的技法を用いた実用的発展
Project/Area Number |
18J22498
|
Research Category |
Grant-in-Aid for JSPS Fellows
|
Allocation Type | Single-year Grants |
Section | 国内 |
Research Field |
Software
|
Research Institution | Kyoto University (2020) The Graduate University for Advanced Studies (2018-2019) |
Principal Investigator |
和賀 正樹 京都大学, 情報学研究科, 助教
|
Project Period (FY) |
2018-04-25 – 2021-03-31
|
Project Status |
Completed (Fiscal Year 2020)
|
Budget Amount *help |
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2020: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2019: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2018: ¥800,000 (Direct Cost: ¥800,000)
|
Keywords | モニタリング / 軽量形式検証 / 物理情報システム / ハイブリッドオートマトン / 探索的テスト / 反例生成 / 時間オートマトン / パラメタ同定 / オートマトン学習 / 回帰型ニューラルネットワーク / ムーアマシン |
Outline of Annual Research Achievements |
まず本年度は、モニタリング対象のシステムの近似的な動作の仮定を用いたモニタリング問題の拡張を行った。具体的には線形ハイブリッドオートマトンで与えられたシステムに近似モデルを用いることで、間欠的にサンプリオングされたログにおいて、二つのサンプルの間での動作についてもモニタリングを行うことができる拡張を行った。このことにより、例えば異常動作の検出漏れを防ぎつつサンプリング周期を伸ばすことが可能となり、組込みシステム等計算資源が限られている環境での応用が期待できる。本研究結果をまとめた論文が物理情報システムに関する国際会議 ICCPS 2021に採択された。
さらに物理情報システムの探索的テストにおける、異なる物理量に言及したさいの困難を解決する研究も行った。異なる物理量間では通常用いられる値の大きさが一般には異なるが、これによって物理情報システムの探索的テストにおいて、ある特定の物理量の変化が事実上無視されてしまうという「スケール問題」という現象が知られていた。本研究では、物理量の絶対的な大きさのみではなく相対的な順位も考慮することで、「スケール問題」を回避しながら探索的テストを行うことのできる拡張を行った。本研究結果をまとめた論文がシステム制御に関する国際会議 ADHS 2021に採択された。
また、前年度に採択された、物理情報システムについての反例生成問題を、オートマトン学習を経由して解く手法について研究成果を物理情報システムに関する国際会議HSCC 2020において口頭発表を行った。更に日本ソフトウェア科学会第37回大会において、前年度に研究を行った[Waga, Andre, & Hasuo, CAV'19]の内容について招待講演を行った。 また,前々年度,前年度,本年度の成果を博士論文として体系化した.
|
Research Progress Status |
令和2年度が最終年度であるため、記入しない。
|
Strategy for Future Research Activity |
令和2年度が最終年度であるため、記入しない。
|
Report
(3 results)
Research Products
(33 results)