| 研究課題/領域番号 |
19H04084
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| 研究分担者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2024-03-31
|
| キーワード | モデル検査 / PDR |
|---|
| 研究実績の概要 |
本研究課題での主要なトピックの一つである仕様手動到達性 (Property Directed Reachability; PDR) を用いたモデル検査手法について，理論面で大きな成果があった．PDRは，従来、実装の詳細を伴う手続き型言語での定義が主流であり，その本質的な計算プロセスが理解しにくい状況であった．そこで我々は，束論 (Lattice Theory) を用いてPDRを理論的に再定義することで，その本質を明らかにする新しい定義を提案した．この新たな定義により，確率的システムをはじめとする様々なシステムに対する PDR が統一的に理解できることを示した．さらに，この定義に基づいた検証器を実装した．この実装は，様々なシステムの性質を差分的に実装することで，そのシステムのためのPDRを自動的に導出できるような一般的な実装となっており，その汎用性が従来実装に比して非常に高くなっている．本研究の成果を，2022年の国際会議 Computer Aided Verification (CAV) において発表した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
上記の CAV での発表を始め，関連する成果が多く上がっており，進捗は順調である．
|
| 今後の研究の推進方策 |
前年度までの強化学習を用いたモデル検査器の高速化手法や，PDR の再定義等の手法をさらに進化させ，IoT において多く現れるハイブリッドシステムの検証手法として結実させる方向に研究をすすめる予定である．
|
