2018 Fiscal Year Annual Research Report
物理情報システムに対する軽量検証の、オートマトン的技法を用いた実用的発展
| Project/Area Number |
18J22498
|
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
和賀 正樹 総合研究大学院大学, 複合科学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2018-04-25 – 2021-03-31
|
| Keywords | モニタリング / 物理情報システム / 時間オートマトン / ムーアマシン / パラメタ同定 |
|---|
| Outline of Annual Research Achievements |
本年度前半は、ネットワークで繋がれている組込みシステムなどにおいて、少ない計算リソースで効率的に時間パターンマッチング問題に対する前処理を行なう、ムーアマシンフィルタを提案・実装し、実験を行った。本研究の結果をまとめた論文は国際会議 EMSOFT 2018に採択され、口頭発表を行い、論文誌 IEEE TCAD に収録されている。本研究については国内学会 PPL 2019にも採択され、口頭発表を行った。
本年度後半は主にフランス・パリ第13大学のEtienne Andre准教授と共に、時間パターンマッチング問題の、入力の仕様がパラメタを含む場合への拡張である、パラメタ付き時間パターンマッチング問題についての研究を行った。まず、パラメタ付き時間パターンマッチング問題を、パラメタ付き時間オートマトンを用いて定式化し、パラメタ付きモデル検査のツールであるIMITATORを用いてパラメタ付き時間パターンマッチング問題を解く手法を提案、実験を行った。本研究の結果をまとめた論文は国際会議 ICECCS 2018に採択され、best paper awardを受賞した。また、(パラメタなし) 時間パターンマッチング問題に対する高速化の手法を、パラメタ付き時間パターンマッチング問題へと拡張する研究も行った。この高速化の手法を用いたアルゴリズムにより、より大きな入力に対して現実的な時間で処理することが可能となった。このアルゴリズムを実装・実験し、結果を論文としてまとめ、国際会議 NFM 2019に採択された。
また、申請者は修士課程在学中に、時間パターンマッチング問題を効率的に解くアルゴリズムをツール MONAA として実装・公開した。この成果は前年度国際ワークショップMT-CPS 2018に投稿され採択されていたが、その口頭発表が本年度申請者によって行われた。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
当初の計画について、計画以上の進展が得られた。まず、当初の研究計画にあった「より本質的な情報を抽出」する手法として、上述のAndre氏と共にパラメタ付き時間パターンマッチング問題を定式化及びアルゴリズムの提案を行ない、トップ国際会議の一つであるICECCS’18 (CORE rank A) に採択され，最優秀論文賞を受けた [Andre, Hasuo & Waga, ICECCS’18]。
さらに、申請者の以前の研究と組み合わせて更なる高速化も達成することができ、NASAの主催する国際会議に採択された[Waga & Andre, NFM’19, accepted]。
また、組込みシステムにおける軽量検証のためのムーアマシンフィルタの提案も行い、組み込みシステム分野のトップ国際会議であるEMSOFT 2018(CORE rank A)において発表された。この成果については特許出願も行った。
|
| Strategy for Future Research Activity |
前年度は「より本質的な情報を抽出」する手法として、パラメタ付き時間パターンマッチング問題について取り組んだ。本年度は、パラメタ付き時間パターンマッチング問題を解くツールの公開を行うとともに、更に多くの情報を抽出できるような手法を構築することを主眼において研究を進める。
また、組込みシステムにおける軽量検証技術についても引き続き改良を進めていく。
|
Research Products
(9 results)
