| Project/Area Number |
22K17873
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
和賀 正樹 京都大学, 情報学研究科, 助教 (00899007)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2024: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2023: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2022: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | 準同型暗号 / 秘匿モニタリング / 時間オートマトン / 記号的オートマトン / ブラックボックス検査 / 能動的MDP学習 / 確率的モデル検査 / 物理情報システム / 軽量形式手法 / オートマトン理論 / 量的検証 |
|---|
| Outline of Research at the Start |
自動運転車やロボット等の高度な信頼性が要求される物理情報システムの開発では、形式検証などを用いたシステマティックな品質保証が重要である。
近年の形式検証の発展の大きな潮流として、1) 危険状態への不達性等の質的な性質に加えて、実行時間や故障確率等の量的な性質をも保証する量的形式検証、2) 網羅性をある程度犠牲にすることで実用性を向上させた\emph{軽量形式検証}、の二方向の拡張がある。本研究ではこれら2つの潮流の合流点として、量的な軽量形式検証の構築を目的とする。本研究の最大の独自性は時間や確率等を陽に扱う量的オートマトンの理論を用いて拡張を行う点である。
|
| Outline of Annual Research Achievements |
本年度は昨年度に引き続き、監視対象となるログを秘匿したままモニタリングすることのできる、秘匿モニタリングについての研究を行った。本年度は昨年度に提案した手法を拡張することで、数値データの演算などの処理を含む仕様に対しても、監視対象のログを秘匿したままモニタリングを行うことのできるアルゴリズムを提案し、計算機実験により実時間モニタリングに適用可能であることを示した。本研究の結果をまとめた論文は現在執筆中である。
また昨年度に引き続き、ブラックボックス検査と呼ばれる自動テスト手法の量的な拡張に関連する研究でも幾つかの成果を挙げた。まず第一に、ブラックボックス検査で無限通りの入力を扱うための基盤となる手法の構築を行った。従来のブラックボックス検査では主に入力として有限通りのアクションを考慮しているが、これは背景にあるオートマトン学習アルゴリズムがアルファベットの有限性に依存しているためである。本年度は記号的オートマトンという、遷移に述語が記述できるオートマトンの学習アルゴリズムを拡張することで、記号的ミーリオートマトンを学習することができるアルゴリズムの提案を行った。本研究の予備的な結果をまとめた論文を日本ソフトウェア科学会第40回大会にて発表し、発表を行った学生が優秀発表賞を受けた。また、従来のブラックボックス検査では離散的な時間概念を考慮したシステムのテストを行っていたが、物理情報システムにおいてはより連続的な時間概念を考慮する方が自然な場合も少なくない。本年度は時間オートマトンという、従来のオートマトンを連続的な時間概念に拡張したオートマトンに対する学習アルゴリズムの提案を行った。本研究の結果をまとめた論文は形式検証に関するトップ国際会議であるCAV 2023に採択され、発表を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画通り時間制約を含むシステムに対するブラックボックス検査のための基盤技術の構築を行い、トップ国際会議で採択されるなど、高い評価を得ている。
実行時モニタリングについても、秘匿モニタリングという当初計画に盛り込んでいなかった内容で実用上の進展があった。
|
| Strategy for Future Research Activity |
引き続き、ブラックボックス検査と実行時モニタリングを量的かつ実用的に拡張する研究を推進する。
|
