2021 Fiscal Year Annual Research Report
| Project/Area Number |
19H04084
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Keywords | モデル検査 / PDR |
|---|
| Outline of Annual Research Achievements |
本研究課題での主要なトピックの一つである仕様手動到達性 (Property Directed Reachability; PDR) を用いたモデル検査手法について，理論面で大きな成果があった．PDRは，従来、実装の詳細を伴う手続き型言語での定義が主流であり，その本質的な計算プロセスが理解しにくい状況であった．そこで我々は，束論 (Lattice Theory) を用いてPDRを理論的に再定義することで，その本質を明らかにする新しい定義を提案した．この新たな定義により，確率的システムをはじめとする様々なシステムに対する PDR が統一的に理解できることを示した．さらに，この定義に基づいた検証器を実装した．この実装は，様々なシステムの性質を差分的に実装することで，そのシステムのためのPDRを自動的に導出できるような一般的な実装となっており，その汎用性が従来実装に比して非常に高くなっている．本研究の成果を，2022年の国際会議 Computer Aided Verification (CAV) において発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
上記の CAV での発表を始め，関連する成果が多く上がっており，進捗は順調である．
|
| Strategy for Future Research Activity |
前年度までの強化学習を用いたモデル検査器の高速化手法や，PDR の再定義等の手法をさらに進化させ，IoT において多く現れるハイブリッドシステムの検証手法として結実させる方向に研究をすすめる予定である．
|
