研究課題/領域番号 |
22K17873
|
研究種目 |
若手研究
|
配分区分 | 基金 |
審査区分 |
小区分60050:ソフトウェア関連
|
研究機関 | 京都大学 |
研究代表者 |
和賀 正樹 京都大学, 情報学研究科, 助教 (00899007)
|
研究期間 (年度) |
2022-04-01 – 2025-03-31
|
研究課題ステータス |
交付 (2023年度)
|
配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2024年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2023年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2022年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
|
キーワード | 準同型暗号 / 秘匿モニタリング / 時間オートマトン / 記号的オートマトン / ブラックボックス検査 / 能動的MDP学習 / 確率的モデル検査 / 物理情報システム / 軽量形式手法 / オートマトン理論 / 量的検証 |
研究開始時の研究の概要 |
自動運転車やロボット等の高度な信頼性が要求される物理情報システムの開発では、形式検証などを用いたシステマティックな品質保証が重要である。 近年の形式検証の発展の大きな潮流として、1) 危険状態への不達性等の質的な性質に加えて、実行時間や故障確率等の量的な性質をも保証する量的形式検証、2) 網羅性をある程度犠牲にすることで実用性を向上させた\emph{軽量形式検証}、の二方向の拡張がある。本研究ではこれら2つの潮流の合流点として、量的な軽量形式検証の構築を目的とする。本研究の最大の独自性は時間や確率等を陽に扱う量的オートマトンの理論を用いて拡張を行う点である。
|
研究実績の概要 |
本年度は昨年度に引き続き、監視対象となるログを秘匿したままモニタリングすることのできる、秘匿モニタリングについての研究を行った。本年度は昨年度に提案した手法を拡張することで、数値データの演算などの処理を含む仕様に対しても、監視対象のログを秘匿したままモニタリングを行うことのできるアルゴリズムを提案し、計算機実験により実時間モニタリングに適用可能であることを示した。本研究の結果をまとめた論文は現在執筆中である。 また昨年度に引き続き、ブラックボックス検査と呼ばれる自動テスト手法の量的な拡張に関連する研究でも幾つかの成果を挙げた。まず第一に、ブラックボックス検査で無限通りの入力を扱うための基盤となる手法の構築を行った。従来のブラックボックス検査では主に入力として有限通りのアクションを考慮しているが、これは背景にあるオートマトン学習アルゴリズムがアルファベットの有限性に依存しているためである。本年度は記号的オートマトンという、遷移に述語が記述できるオートマトンの学習アルゴリズムを拡張することで、記号的ミーリオートマトンを学習することができるアルゴリズムの提案を行った。本研究の予備的な結果をまとめた論文を日本ソフトウェア科学会第40回大会にて発表し、発表を行った学生が優秀発表賞を受けた。また、従来のブラックボックス検査では離散的な時間概念を考慮したシステムのテストを行っていたが、物理情報システムにおいてはより連続的な時間概念を考慮する方が自然な場合も少なくない。本年度は時間オートマトンという、従来のオートマトンを連続的な時間概念に拡張したオートマトンに対する学習アルゴリズムの提案を行った。本研究の結果をまとめた論文は形式検証に関するトップ国際会議であるCAV 2023に採択され、発表を行った。
|
現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初の計画通り時間制約を含むシステムに対するブラックボックス検査のための基盤技術の構築を行い、トップ国際会議で採択されるなど、高い評価を得ている。 実行時モニタリングについても、秘匿モニタリングという当初計画に盛り込んでいなかった内容で実用上の進展があった。
|
今後の研究の推進方策 |
引き続き、ブラックボックス検査と実行時モニタリングを量的かつ実用的に拡張する研究を推進する。
|