| 研究課題/領域番号 |
22K17873
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
和賀 正樹 京都大学, 情報学研究科, 助教 (00899007)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
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つの潮流の合流点として、量的な軽量形式検証の構築を目的とする。本研究の最大の独自性は時間や確率等を陽に扱う量的オートマトンの理論を用いて拡張を行う点である。
|
| 研究実績の概要 |
本年度は主にハイパー性質と呼ばれる、従来主に扱われてきたトレース性質を一般化した性質に対する軽量形式検証に取り組んだ。ハイパー性質の例として、様々な入力に対して公平な挙動をするという公平性や、外部からの入力が同じであれば外部からの観測の上では常に等価な振舞いをするという観測決定性などがある。
まず実行時モニタリングにおいて、これまでに提案されてきたトレース性質に関するモニタリング手法を、ハイパー性質を扱えるような拡張に取り組んだ。具体的にはハイパー性質に関するモニタリングを行う際に、単に要求仕様の違反を検出するのみではなく、違反の具体的な証拠となる実行箇所を提示できる、ハイパーパターンマッチングという問題を提案・定式化し、効率的に解くアルゴリズムの提案を行った。本研究の成果をプロトタイプツール HypPAu として実装し、計算機実験や理論的な解析結果をまとめた論文を執筆し、現在査読中である。
また、ハイパー性質に関する形式検証手法にも取り組んだ。連続的時間概念の下で、時間制約中に未知のパラメタを含むようなシステムモデルが、同様に時間制約中に未知のパラメタを含むようなハイパー性質を充たすことを網羅的に検証するモデル検査アルゴリズムを提案した。本研究の成果をプロトタイプツール HyPTCTLChecker として実装し、計算機実験や理論的な解析結果をまとめた論文を執筆し、組込システムに関するトップ国際会議 EMSOFT 2024 にて採択された。本形式検証手法と前年度に提案した時間オートマトンの学習手法などを組み合わせることで、連続的時間概念の下でのハイパー性質に関するブラックボックス検査への応用が期待される。
|
| 現在までの達成度 |
現在までの達成度
2: おおむね順調に進展している
理由
ハイパー性質に関する軽量形式検証という当初計画に盛り込んでいなかった内容で理論・実用上の進展があった。当初計画していた、時間制約を含む仕様に対するブラックボックス検査についても、特にハイパー性質を取り扱うための基盤技術の構築を行い、トップ国際会議で採択されるなど、高い評価を得ている。
|
| 今後の研究の推進方策 |
来年度も引き続き、ハイパー性質を初めとした様々な性質に関するブラックボックス検査と実行時モニタリングを量的かつ実用的に拡張する研究を推進する。
|
